D enters Tiobe top 20

[Ola Fosheim Grøstad]

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.

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

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.

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

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.

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