D enters Tiobe top 20
x at x.com
Fri Nov 8 16:10:32 UTC 2019
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
> I read it as ensuring the interface to the unsafe code is
> correct, not the unsafe code itself. I.e. "is properly
> 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:
> 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:
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.
More information about the Digitalmars-d