D enters Tiobe top 20

[Ola Fosheim Grøstad]

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.