D enters Tiobe top 20

[Doc Andrew]

On Friday, 8 November 2019 at 18:51:42 UTC, Ola Fosheim Grøstad 
wrote:
> 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.

I'm WAAAYYY out of my pay grade here, but I _think_ the 
distinction may depend on the underlying logic that the solver is 
using. Something like Coq where your Naturals are built on 
successor types would probably have a hard time with the modular 
arithmetic, but it might just not be a big deal for the Why3 
solvers which I _think_ are using Hoare logic, since that's what 
HOL/ML is built on. I'm not really an expert in the Hoare logic 
though, and know just enough Coq to embarrass myself :) The Why3 
solver will also let you use Coq to do a manual proof in the 
event that the automated prover can't figure it out, so I can't 
say for sure.