D enters Tiobe top 20

[Ola Fosheim Grøstad]

On Sunday, 10 November 2019 at 04:15:08 UTC, Doc Andrew wrote:
> 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!

Sounds like you have set a course that you can follow!

I would personally just have ignored templates and extended one 
of the linty D-parser, as I think it will lead to a more 
transparent codebase that is easier to experiment with than 
modifying the D compiler.

But maybe you'll find that doing it within dmd from start works 
out for you. The plain dmd compiler should not so difficult to 
set up, so just try it, I guess?

You could build your own VC-ast from the D-ast, then manipulate 
it and emit VC-code.

> 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.

Yes, I don't know,  what is most important is that you think it 
is important enough to carry the burden on your own for at least 
a year. Over time, surely others will come along that share that 
viewpoint. Just keep the codebase simple so that people with no 
FV knowledge can contribute... In the beginning there will 
basically be no advantages to using the tool, so... it takes a 
lot of patience.

Maybe a well written DIP can bring people on board from the 
start, but I haven't seen many people interested in FV when that 
topic has been discussed in the forums. Again, just try, I guess?