D enters Tiobe top 20
Ola Fosheim Grøstad
ola.fosheim.grostad at gmail.com
Fri Nov 8 10:38:15 UTC 2019
On Friday, 8 November 2019 at 10:25:44 UTC, Walter Bright wrote:
> 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.
They probably mean that it is verified with human provided guides.
A human must annotate the library with carefully chosen asserts
that the verifier will prove one-by-one until they can all be
disposed of. So you have to understand that verification engine
and carefully "nudge" it until it succeeds.
So, mostly suitable for the standard library and simple third
party libraries, but not for bleeding-edge applications that keep
changing...
More information about the Digitalmars-d
mailing list