D enters Tiobe top 20

[Ola Fosheim Grøstad]

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:

https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html#integers

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