1. 49

In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. 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.

  1.  

  2. 14

    From the Adrian Colyer’s review, we find the title might be misleading depending on what ownership model entails for a given developer’s use of the language:

    “We had to make some concessions in our modelling: we do not model…”

    1. more relaxed forms of atomic accesses, which Rust uses for efficiency in libraries like Arc

    2. Rust’s trait objects, which can pose safety issues due to their interactions with lifetimes

    3. stack unwinding when a panic occurs, which can cause similar issues to exception safety in C++

    4. automatic destruction, “which has already caused problems for which the Rust community still does not have a modular solution.”

    5. a few details unrelated to ownership, such as type-polymorphic functions and “unsized” types.”

    Also shows why it’s good to have a semantics in the beginning covering the whole language like with ML or later SPARK Ada. It forces language developers to spot and address these corner cases early on. Good news is that, like with SPARK, one might just subset their use of Rust to exclusively what has been proven with no use of anything else. Is anything on the list common enough in most Rust development where it can’t be avoided and must be verified later? I’ve obviously seen many people mention traits. Arc and automatic destruction safety not being proven is a bit ironic given they’re presumably there to boost safety versus raw pointers and manual destruction.

    1. 4

      Got two, nice responses on HN about how much these may or may not matter:

      https://news.ycombinator.com/item?id=16303229

      It’s looking like a subsetting approach can keep one within what’s in the proven model.

    2. 7

      Lobsters had a long discussion of this paper 7 months ago.