rust-memory-model

he memory model. This gives a formal definition of what kinds of aliasing assumptions the compiler is able to make about raw pointers in `unsafe` code. This is being worked on here: https://github.com/nikomatsakis/rust-memory-model 2. The borrow checker. While the RustBelt work shows that a much simpler borrow checker can be sound, Rust's borrow checker has to deal with a much more complicated language, and there are few known soundness bugs in it (discussed elswhere in this thread). You'd want that to be formally modeled and verified. 3. The type system. Rust has a fairly full featured type system, so you want to ensure that's sound 4. The compiler itself. Even once you have sound code in a sound language, you need to make sure that the compiler follows the rules and compiles it correctly. 5. Any libraries or code that you are using which might be using `unsafe`. The RustBelt work so far has done so for a few core primitives, as well as a couple of third-party libraries, but of course you'd want to re-do this work against the full language (or a real-world subset, not LambdaRust that this paper used) and include any other libraries that you might need to use. So, I'd say that there's a good chance that the RustBelt work could be extended to include one or more of these listed features before all of the rest of the above has been done. It will be a while before you could have a usable, verified subset of Rust, but once you do I think it could be a good alternative to something like SPARK, or development in C following extremely stringent rules and compiling with CompCert.

all other modules which use `unsafe` code as well? That was in many ways quite a big question about the design of Rust; can you prove or very each module which uses `unsafe` independently? The borrow checker, on the other hand, is an entirely local analysis. It can get quite complex, especially as you allow for more fine-grained borrow checking to make it convenient to use compound objects, and introduce non-lexical lifetimes which help reduce the number of restrictions on what you can do, but since it's entirely local, it's a much more tractable problem. I think that it would be good to eventually formalize the full Rust borrow checker, and of course it's always good to fix these soundness bugs, but there are some more important open questions right now like fully specifying Rust's memory model (https://github.com/nikomatsakis/rust-memory-model) so it's possible to know what kinds of aliasing you can actually do in `unsafe` code, and which will be safe even under future versions of the compiler. The RustBelt work so far is just a nice foundation getting Rust to be more formally analyzed and specified. There's a lot of work left to be done.