D enters Tiobe top 20

[Doc Andrew]

On Friday, 8 November 2019 at 17:55:41 UTC, Ola Fosheim Grøstad 
wrote:
> On Friday, 8 November 2019 at 17:07:59 UTC, Doc Andrew wrote:
>> For sure - but there may be a _useful_ formally-verifiable 
>> subset of D buried in there somewhere, kind of like MISRA C.
>
> I guess it is worth mentioning though that all integers in D 
> follow the semantics of modular math, so you would not be able 
> to conduct proofs with the assumption that you work with 
> natural integers. So you cannot assume that "x+1 > x" for any 
> type in D, that might make many proofs more difficult.
>
> Modular math can be handled with bit-blasting (turning each bit 
> to a logic expression and use SAT), but maybe with less success.

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. That's what SPARK does, at least. If the 
modular arithmetic is desired you'd probably have to manually put 
the overflow check and reassignment to 0 (or whatever) in there.

That's one kind of annoying thing I discovered about Rust when 
working on some crypto code - having to write Wrapping types all 
over the place. The bad thing there was that the overflow checks 
were only in Debug mode, so in Release mode the code worked as 
intended without Wrapping. That was a few years ago, so things 
may be a little different now.