D enters Tiobe top 20

[Doc Andrew]

On Friday, 8 November 2019 at 16:33:48 UTC, Ola Fosheim Grøstad 
wrote:
> On Friday, 8 November 2019 at 16:10:32 UTC, Doc Andrew wrote:
>> With sufficient pre & post-conditions on "unsafe" functions, 
>> (and maybe, as somebody pointed out, some asserts along the 
>> way to "nudge" the solver in the right direction), you can 
>> prove at that nothing bad happens with an automated solver.
>
> If you talk only about memory safety and require that programs 
> are written in a certain way, then maybe yes.
>
> In the general case this will not be possible though. You 
> certainly need to manually guide the verifier (e.g. "nudge" the 
> solver with asserts). The search space is vast. Keep in mind 
> that when humans do proofs in math they do a lot of pattern 
> matching, use a high level conceptualization of the problem 
> space and only do it on "toy-sized" problems.

Sure, one reason SPARK is amenable to FV is because the language 
restrictions and richness of Ada types does a lot to restrict 
that search space, the same way dependently-typed languages do.

>
>> I'm not an expert, and it's only a hunch, but I suspect that 
>> DbC + CTFE could make formal verification of D code a lot 
>> easier to implement than trying to graft it on to other 
>> languages.
>
> Formal verification is never easy, but certainly less difficult 
> when the programming language is designed with that in mind... 
> D is too flexible.

For sure - but there may be a _useful_ formally-verifiable subset 
of D buried in there somewhere, kind of like MISRA C.

>
> And that's only for single-threaded programs. Add 
> multi-threading and you basically need the programming language 
> to be designed for it to get anywhere realistic. Such languages 
> do exist, but they are not going to give you C-performance.
>

With the way we do multi-threading now, where anything goes, 
absolutely. SPARK can formally verify multi-threaded tasks but 
using a fairly restrictive model (Ravenscar). I don't think 
performance goes absolutely in the tank with Ravenscar, but yeah, 
if you don't worry about synchronization, ignore race conditions, 
and just hope for the best, then sure, you're going to win in the 
benchmarks :)

I look at it a little differently - multi-threaded code is so 
tough to get right that some sort of verified correctness for it 
is becoming _essential_. (see: 
https://www.phoronix.com/scan.php?page=news_item&px=Google-KCSAN-Sanitizer)

It may be that a slightly-different threading model, perhaps like 
that thread "nursery" idea which has been posted here before 
(https://vorpus.org/blog/notes-on-structured-concurrency-or-go-statement-considered-harmful/) will be a magic bullet... or not.

>> My take is that formal verification is sort of where AI/ML was 
>> 20 years ago - academically interesting but of little 
>> practical use. Now it's a big deal, and I think in 10-20 
>> years, FV will be too.
>
>  I think FV is where AI was 70 years ago...

Way too pessimistic! :)

>
> But yeah, maybe neural networks can be used for matching up 
> verification problems with strategies so that the verifier 
> succeeds more frequently, but the fact that an automated 
> verifier frequently will fail to reach any conclusion will 
> remain for practical programming that aim for very high 
> performance in the forseeable future.

One thing that I've looked around for (without much luck) is just 
using GPUs to speed up the solvers themselves. Apparently 
parallelizing SAT solvers isn't the easiest thing in the world, 
but it would be a neat research topic.

>
> A more likely future is that processing performance will be in 
> abundance and that you therefore don't have to write programs 
> that maximize performance and can switch to languages and 
> algorithms that are easier to prove correct...

The cool thing is that, with the right proofs in place, you can 
actually get _faster_ code when formally verified, because all of 
the normal sanity-checks you do in code can get shifted to 
compile-time. You might even be able to reduce  or eliminate 
thread blocking, etc. with the right model (and probably some HW 
assistance).

Your point is well taken, but I do hope that we can get proven 
correctness of bare-metal code without having to write something 
like Liquid Haskell ;)

-Doc