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