D enters Tiobe top 20

[Doc Andrew]

On Friday, 8 November 2019 at 22:41:23 UTC, Walter Bright wrote:
>
> assert()s are the contracts that matter, not the in and out 
> contracts, which can be replaced with assert()s. In no way did 
> I mean to imply that assert()s were a mistake!
>
> I've thought for 35 years that assert()s can be the input to a 
> program prover, i.e. it's nothing new, but I do not have the 
> expertise to figure out such proofs might work, other than 
> simplistic cases.

Now you've done it. I've seen this before, right before templates 
were in D. This is where you disappear for a couple of weeks and 
then come back to announce that D can formally verify user code, 
right? :)

The in/out syntax doesn't add a lot for typical function body 
code, since everything is in sequential order anyhow, but in 
interfaces they would be essential. They may be under-utilized, 
but I think they might just be one of those features that is a 
late bloomer. I wouldn't consider taking them out of the language 
just yet, even for regular functions.

Proving properties of D code outright is probably tough, but 
doing a mechanical conversion (of at least some subset of D, 
maybe betterC) to an intermediate language like ML and then 
feeding it into a solver is probably possible. Here's an 
interesting project I found that can generate Why code from 
LLVM-IR: https://github.com/AnnotationsForAll/WhyR. It might be 
interesting to throw some LDC IR at it and just see what happens!

Given that D already has contracts in place, using them to 
generate Why's "ensures" and "requires" clauses would be much 
easier than something like C where you'd need specially-formatted 
comments or a language extension.

Even without specific contracts, a list of things that you _know_ 
are run-time errors (divide-by-zero, null-pointer dereference, 
etc.) could be proven absent from code. The nice thing about an 
approach like this is that you don't have to change the language 
or mess with the compiler, instead the prover is just another 
tool, like a linter, that you can use if you need it.

Not everybody is as optimistic as I am, but I do believe that 
with the emphasis on safety these days, I suspect FV will become 
a requirement in the future.

-Doc