D enters Tiobe top 20

[Doc Andrew]

On Sunday, 10 November 2019 at 00:31:18 UTC, Ola Fosheim Grøstad 
wrote:
>
> A fun way to get started might be to create your own verified 
> mini-language and compile it to D code and use that as a 
> proof-of-concept.

So that brings up the question of which approach to use.

The idea you mentioned there is how F* (or at least the subset 
"Low"), Coq, and probably some others I can't think of - do it. 
You write verified functional code, run it either through an 
automated solver or write proofs manually, and then "extract" a 
compile-able (basically C) or interpret-able (OCaml, Scheme, 
Haskell...) program in another language from it. For C, I think 
usually they target the CLight dialect of C, so they can use the 
CompCert verified compiler 
http://compcert.inria.fr/doc/index.html.

The cool thing here is that you can basically guarantee that the 
assembly that's generated matches the specifications of the 
original code. I consider this approach the 
"Obsessive-Compulsive" method. This is for the programmer who 
just _knows_ that there's a compiler bug causing his code to be 
wrong. :) This is more suited towards the goal of a totally 
verified toolchain.

(Side note: There's a certain, say, "academic" beauty in thinking 
that you've got "turtles all the way down" with a totally 
verified language and toolchain. But there's always going to be 
hardware bugs, cosmic rays, out-of-memory conditions, etc.)

Personally, I'm less worried about what DMD, GCC or LDC might 
have gotten wrong than what _I_ goofed up in my own code, so this 
option isn't super appealing to me.

Eventually, I'd love for my compiler, standard library, OS, etc. 
to be formally-verified. But... they're probably not going to be 
written in Coq or ML, if we're being honest. D or Rust? More 
probable - so we get to option 2:

Option 2, taken by Dafny and SPARK (and I think FRAMA-C too, but 
don't quote me on that), is take the language you want (or at 
least something close), then generate an intermediate language 
that can be easily broken down into verification conditions to 
run through the solver.

For formally-verified D, this is the route I'd want, because I 
like writing D!

Writing a verified language that extracts to D is sort of a 
dead-end, in my opinion. It doesn't make people's D code any 
safer, and if I'm going to extract to a compiled language, then I 
might as well decide on C/CLight and take advantage of CompCert 
or some other toolchain that's been verified already, or just use 
GCC and get wider platform exposure.

Option 3 is to just take the language as it is and try to 
generate some kind of formal logic based on the language 
constructs as you parse it, then work out the solver mechanics or 
some kind of proof assistant for working through it. There might 
be _somebody_ out there that could take this on, but it ain't me!

A lot of smart people have already worked out automated provers 
for ML-ish languages, and D is unique in that it already has nice 
contract syntax that could map nicely to the axioms and 
verification conditions that those languages use.

I suspect that ultimately, we could get what we need by taking 
some intermediate DMD front-end state (maybe AST + UDA __traits), 
doing flow analysis, and dumping out (a lot of) some intermediate 
verification language with the assertions baked in and run an 
existing proof tool on it. You'd have to do some gonkulation of 
the solver output to figure out what your original line of code 
was for sensible error messages, but that's possible.

Microsoft's VCC multithreaded C verifier tool might be a good 
starting point, since it's got a friendly license (MIT) - 
https://github.com/microsoft/vcc. It uses Boogie, too. SPARK (the 
GNATProve tool, specifically) is all GPLed, so not sure if it's a 
good resource or not. IANAL and all that.

That's an almost criminally-understated view of the task, but I 
think it might give D a path towards FV, if people think it's 
worth it. D has always been on the cutting edge of good SW 
engineering support in a language, so who knows?

-Doc