RustBelt: Computer Scientist proves safety claims of Rust programming language

eurekalert.org

28 pointslsllc2 comments

He 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.

> RustBelt is a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. [1]