D enters Tiobe top 20

Ola Fosheim Grøstad ola.fosheim.grostad at gmail.com
Fri Nov 8 17:55:41 UTC 2019


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.



More information about the Digitalmars-d mailing list