D enters Tiobe top 20

Ola Fosheim Grøstad ola.fosheim.grostad at gmail.com
Fri Nov 8 18:51:42 UTC 2019

On Friday, 8 November 2019 at 18:39:25 UTC, Doc Andrew wrote:
> 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).

Hm, seems to me that it has signed integers with bounds that are 
non-modular and unsigned integers that are modular:


So, in that case a prover could model bounded integers as 
integers with a constraint, and modular unsigned integers as 

More information about the Digitalmars-d mailing list