D enters Tiobe top 20

[Doc Andrew]

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).