It protects until you need to disable that protection to actually program a solution in Rust.C cannot protect a programmer from making certain mistakes whereas Rust does. Yes all such languages work at an unsafe level under the hood where machine instructions are used but Rust can and does strictly and explicitly isolate unsafe code.
Have a read of this: Computer Scientist proves safety claims of the programming language Rust
That's proof in the mathematical sense, as in we can prove the square root of two is irrational, that kind of proof.
So if the team are all writing safe Rust code these kinds of errors simply cannot happen, ever, ever, ever - that is a huge improvement in quality.
From the link you supplied .
In other words you need a knife (external program "Miri') too just like with C to check for correctness in the land-mine field. I've seen lots of CS mathematical proofs be junked because they don't prove physical correctness in non-deterministic conditions like hardware interfacing.Sometimes, however, it is necessary to write an operation into the code that Rust would not accept because of its type safety," the computer scientist continues. "This is where a special feature of Rust comes into play: programmers can mark their code as 'unsafe' if they want to achieve something that contradicts the programming language's safety precautions.
...
This proof, called RustBelt, is complemented by Ralf Jung with a tool called Miri, with which 'unsafe' Rust code can be automatically tested for compliance with important rules of the Rust specification - a basic requirement for correctness and safety of this code.
I looked the proof and the preconditions and limitations.
https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf
Mathematical proofs relate to exactly how a MODEL will behave. They don't have much to do with how the real world behaves.9 CONCLUSION
We have described λRust, a formal version of the Rust type system that we used to study Rust’s
ownership discipline in the presence of unsafe code. We have shown that various important
Rust libraries with unsafe implementations, many of them involving interior mutability, are safely
encapsulated by their type. We had to make some concessions in our modeling: 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 (comparable to interfaces in Java), which can pose safety issues due to their
interactions with lifetimes; or (3) stack unwinding when a panic occurs, which causes issues similar
to exception safety in C++ [Abrahams 1998]. We proved safety of the destructors of the verified
libraries, but do not handle automatic destruction, which has already caused problems [Ben-Yehuda
2015b] for which the Rust community still does not have a modular solution [Rust team 2016]. The
remaining omissions are mostly unrelated to ownership, like proper support for type-polymorphic
functions, and “unsized” types whose size is not statically known12
Last edited: