Friday 27 January 2017
Most academic CS research projects strike me as somewhere between "could be useful" and "hahahaha no". Rustbelt is one of the very few in the category of "oh please hurry up we need those results yesterday". That's exactly the sort of project researchers should be flocking to.
The long-term goal here is to specify formal semantics for Rust's safe and unsafe code and have a practical, tool-supported methodology for verifying that modules containing unsafe code uphold Rust's safety guarantees. This would lead to an ecosystem where most developers mostly write safe code and that's relatively easy to do, but some developers sometimes write unsafe code and that's a lot harder to do because you have to formally verify that it's OK. In exchange, you know that your unsafe code isn't undermining the benefits of Rust; it's "actually safe". I think this would be a great situation to have. We need the results as soon as possible because they will suggest changes to Rust and/or what is considered "valid unsafe code", and the sooner they happen, the easier that would be.