D enters Tiobe top 20
timon.gehr at gmx.ch
Fri Nov 8 12:11:26 UTC 2019
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
>>> "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.
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
> 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
> 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:
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
> 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.)
More information about the Digitalmars-d