D enters Tiobe top 20

[Walter Bright]

On 11/8/2019 2:09 AM, Timon Gehr wrote:
> On 08.11.19 04:43, Walter Bright wrote:
>> I don't see anything on that site that contradicts what I wrote. In particular:
>>
>> "Rust's core type system prohibits the aliasing of mutable state, but this is 
>> too restrictive for implementing some low-level data structures. Consequently, 
>> Rust's standard libraries make widespread internal use of "unsafe" blocks, 
>> which enable them to opt out of the type system when necessary. The hope is 
>> that such "unsafe" code is properly encapsulated, so that Rust's 
>> language-level safety guarantees are preserved. But due to Rust's reliance on 
>> a weak memory model of concurrency, along with its bleeding-edge type system, 
>> verifying that Rust and its libraries are actually safe will require 
>> fundamental advances to the state of the art."
>>
>> is saying the same thing.
> 
> 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".