D enters Tiobe top 20

[Doc Andrew]

On Friday, 8 November 2019 at 18:39:25 UTC, Doc Andrew wrote:
> On Friday, 8 November 2019 at 18:25:02 UTC, Ola Fosheim Grøstad 
> wrote:
>> On Friday, 8 November 2019 at 18:11:39 UTC, Doc Andrew wrote:
>>> It works if you explicitly mark overflow as an error. You can 
>>> try to prove that x <= x.max for a given path, and if you 
>>> can't, then you just flag a warning.
>>
>> So you manually assert it then? I guess you could use a 
>> templated type with asserts builtin.
>> But then the solver have to figure out when to designate the 
>> type as an integer and when to designate it as a bitvector. I 
>> guess there is some room for that... perhaps.
>>
>> Another approach is to first prove the code correct for 
>> natural numbers and then try to prove that there is some upper 
>> limit and select an integer size that can contain that upper 
>> limit (e.g. 64 bits vs 32 bits). I am not sure about Dafny, 
>> but I think Whiley backends do that.
>
> With SPARK you don't have to manually assert the checks, it 
> does the overflow checks as part of it's proof automatically. 
> The neat thing is that you define new modular types with their 
> range of allowable values, so as you prove the code, you show 
> that those bounds aren't exceeded. It's basically a type 
> invariant contract as part of the type definition itself (as I 
> understand it).

It's probably worth noting too that SPARK just translates the 
type definitions it sees into Why3 ML code, and uses that in the 
Why3 meta-solver for the proof. It separates proof from 
compilation, so if the proof checks out, then you can compile 
into bare-metal machine-code. This is a little different than a 
lot of the FV languages which take an ML/FP-ish language (with 
GC, etc.) and then have a C backend for it (with a runtime, 
usually).