D enters Tiobe top 20

[Doc Andrew]

On Friday, 8 November 2019 at 10:25:44 UTC, Walter Bright wrote:
>> 
>> Indeed, but more importantly, this group is working on 
>> verification techniques for unsafe Rust code, so it is likely 
>> that unsafe Rust libraries will be proved correct in the 
>> future.
>
> I read it as ensuring the interface to the unsafe code is 
> correct, not the unsafe code itself. I.e. "is properly 
> encapsulated".
>
> After all, if the unsafe code can be proved correct, then it is 
> no longer unsafe, and Rust's ownership/borrowing system can be 
> dispensed with entirely as unnecessary for safety.
>
> I'm happy to let the CS Phd's work on those problems, as I am 
> way out of my depth on it.
>
> I've convinced myself that the Ownership/Borrowing notion is 
> sound, but have no idea how to formally prove it.
>
>> There is also this recent work on functional verification of 
>> safe Rust code: 
>> http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?media=papers:prusti.pdf
>
> I don't see any reason why the techniques used in the paper 
> wouldn't work on D, given O/B.
>
> Note that the paper says: "We do not address unsafe code in 
> this paper".

The AdaCore/SPARK folks have done a lot of related work here that 
might be useful: 
https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memory-Management-in-Ada-and-SPARK.pdf

They took the pointer borrowing idea from Rust and plugged it 
into the SPARK solver (Why3) so formal correctness is guaranteed.

I am very bullish on formal verification in languages going 
forward. The one big advantage that D has in this arena is DbC. I 
was disappointed in your NWCPP talk that you listed it as a 
"miss." :) The potential here is huge! I think it's entirely 
possible that we can do _compile-time_ proofs that D contracts 
can be satisfied.

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. A couple of other 
contract types like loop & type invariants might also be 
necessary (they are in SPARK, at least). It would be pretty cool 
if you had to mark a function as unsafe only if the compiler 
(with some help) couldn't prove otherwise.

If Rust is going the route of a team of pros doing manual proofs 
in Coq to demonstrate absence of errors in "unsafe" code, they're 
in for a world of pain, frankly. My understanding is that the 
formal verification efforts in Rust were more geared towards 
proving that the Rust language/compiler themselves were sound, 
rather than giving Rust users a way of proving correctness of 
their own code, but I may be mistaken. The paper you linked shows 
the opposite, though.

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. The PhD 
students can tell me if I'm wrong :)

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.

-Doc