4 ms·
RustBelt: Computer Scientist proves safety claims of Rust programming language
- rurban 5y agoHe only proves type safety, and layed out ways to prove special type safeties even in type-unsafe code. He didn't tackle the two other rust unsafeties, memory and concurrency.
- phlip9 5y ago> RustBelt is a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. [1] [1] https://people.mpi-sws.org/~jung/thesis.html https://people.mpi-sws.org/~jung/thesis.html