D enters Tiobe top 20
Ola Fosheim Grøstad
ola.fosheim.grostad at gmail.com
Fri Nov 8 18:57:13 UTC 2019
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.
More information about the Digitalmars-d