D enters Tiobe top 20

[Timon Gehr]

On 08.11.19 11:25, Walter Bright wrote:
> 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".
> ...

Read the next sentence after that. In general, feel free to read it any 
way you like, but that's not going to change the goals of the project, 
which correspond to my summary.

https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf

Last sentences in abstract: "Our proof is extensible in the sense that, 
for each new Rust library that uses unsafe features, we can say what 
verification condition it must satisfy in order for it to be deemed a 
safe extension to the language. We have carried out this verification 
for some of the most important libraries that are used throughout the 
Rust ecosystem."

> 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.
> ...

That stance makes little sense. The proofs are manual. As an analogy, 
it's a bit like saying "if it is realistic to audit @trusted functions, 
we can just mark the entire codebase @trusted, obtaining memory safe 
code without any of the @safe restrictions". The difference is that 
here, the proofs can be checked by the computer, but that doesn't make 
them much easier to provide.

> I'm happy to let the CS Phd's work on those problems, as I am way out of 
> my depth on it.
> ...

I understand, but I can't help but notice that you often choose to 
contradict what they are saying on those issues anyway. The bird's-eye 
perspective you would get from an understanding of program verification 
and dependent type theory would help a lot for the design of sound and 
expressive type system extensions, such as O/B for D.

> I've convinced myself that the Ownership/Borrowing notion is sound, but 
> have no idea how to formally prove it.
> ...

One way is to embed it into separation logic. It's in the paper below.

>> 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,

Indeed, separation logic "works" on any language:
https://vst.cs.princeton.edu/download/VC.pdf
https://vst.cs.princeton.edu/veric/

The reason why you want both @safe and @system code is that most 
programmers are unable or unwilling to manually carry out memory safety 
proofs for all the code they write.

> given O/B.
> ...

Sure. Given O/B of the same caliber, you would get a similar 
simplification of correctness proofs. But right now we don't have 
correctness proofs at all, and a lot of times when program verification 
came up on this newsgroup it was rejected with a vague reference to the 
halting problem.

> Note that the paper says: "We do not address unsafe code in this paper".

(I'm aware, having read the paper. Which is of course why I described it 
as "functional verification of _safe_ Rust code". They also refer to 
RustBelt for verification of unsafe code.)