RustBelt: securing the foundations of the Rust programming language

Adrian Colyer did a good write up of this paper recently on The Morning Paper : https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-fo...

Does this prove that the current borrowck rules are sufficient to catch all possible mistakes? For example, does it catch stuff like https://github.com/rust-lang/rust/issues/31287 or https://github.com/rust-lang/rust/issues/38899?

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.

EDIT: Thanks for quick, clarifying replies about these. It's looking like a subsetting approach can work.

I have recently performed a relatively simple development by using programming languages on which I had low-to-to-no experience: Perl (low), Ruby (no), Rust (no) and Go (no). Note that I am quite adaptable on the programming language front and that this small experiment was precisely meant to showcase these adaptability skills. Rust was, by far, the most difficult-to-learn, difficult-to-research, counter-intuitive, unfriendly, constrained, unappealing, etc. of all of them. Warnings and errors appeared systematically and, despite their verbosity, were rarely helpful.

The most ironic part is that so many restrictions and problems are likely to provoke people to rely on whatever option happens to work, which might not be the best/safest one. Being so concerned about making sure that the generated code is extremely safe no matter what by sacrificing flexibility and user friendliness is far from ideal. Restrictions and prohibitions have always to be seen as an in-the-worst-case-scenario resource, not as a primary solution; much less when dealing with something as complex as programming, a very powerful tool supposed to be managed by knowledgeable individuals. The higher the freedom, the better the results delivered by a sensible/knowledgeable person. Unless Rust changes a lot, I don't see it going anywhere. It might get some support from theoretical/academical/inside-whatever-bubble circles, but seriously doubt that developers with real-world experience can like or even accept most of what this language represents.

Rust is a direct contender to C and C++, not to script or GC languages. Please compare apples to apples.