References to Implementation (choices) and proofs regarding memory safety

Hello everybody!

I am interested in the guarantees Rust is giving. especially regarding memory safety. I have a hard time to find some resources on the background of concepts like ownership, lifetimes and the borrow checker.
I got questions like:
What are the exact guarantees given? Is there some (formal) proof, that the language features indeed achieve them?
How exactly is the lifetime system and borrow checker working? (The Rustonomicon in the end gave me a rough a idea but i got no deep understanding)
Maybe you can point me at some documentation on internal implementations or some publications covering the internal design of the language?

Thanks in advance and kind regards,

1 Like

You may also be interested in the RustBelt project, led by Derek Dreyer. Ralf Jung's work on pinning down what's required for unsafe code to be correct is part of RustBelt. Dr. Dreyer was also the advisor of Rust's own Aaron Turon.

Summary of the RustBelt project proposal

A longstanding question in the design of programming languages is how to balance safety and control. C-like languages give programmers low-level control over resource management at the expense of safety, whereas Java-like languages give programmers safe high-level abstractions at the expense of control.

Rust is a new language developed at Mozilla Research that marries together the low-level flexibility of modern C++ with a strong "ownership-based" type system guaranteeing type safety, memory safety, and data race freedom. As such, Rust has the potential to revolutionize systems programming, making it possible to build software systems that are safe by construction, without having to give up low-level control over performance.

Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold. To rule out data races and other common programming errors, 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.

In this project, we aim to equip Rust programmers with the first formal tools for verifying safe encapsulation of "unsafe" code. Any realistic languages targeting this domain in the future will encounter the same problem, so we expect our results to have lasting impact. To achieve this goal, we will build on recent breakthrough developments by the PI and collaborators in concurrent program logics and semantic models of type systems.

1 Like

Thank you, jimb. Indeed that project is pretty interesting regarding the proof part.
I just started getting an overview over the papers.
Do you maybe also have a idea, on where to get more information on how the lifetime system and borrow checker works?

Thanks kornel!
Actually it slightly misses my point of interest, as the link is rather about formally verifying that a Rust program meets its specification than about a general proof of the Language feature guarantee claims like memory safety.
Still interesting (and also helpful, as it pointed me to the RustBelt project already some hours before jimb mentioned it )

I am confused. Are they the same thing? See, for example their slide show, page 19.

As far as I understand (I am a newbie and only an amateur of programming), they gave an operational semantic for lambda-rust, in which each access is valid if the program is well-typed. See the comments after Theorem 7.2.