D enters Tiobe top 20

[Ola Fosheim Grøstad]

On Friday, 8 November 2019 at 18:53:49 UTC, Doc Andrew wrote:
> It's probably worth noting too that SPARK just translates the 
> type definitions it sees into Why3 ML code, and uses that in 
> the Why3 meta-solver for the proof.

Ah, got it :) I haven't looked at Why3 yet.

> This is a little different than a lot of the FV languages which 
> take an ML/FP-ish language (with GC, etc.) and then have a C 
> backend for it (with a runtime, usually).

Yeah, high level FV languages can just do like Python and have 
unbounded integers and such.