RustBelt: securing the foundations of the Rust programming language
https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-foundations-of-the-rust-programming-language/ [blog.acolyer.org]
2018-01-18 19:42
We’d really like to know whether those claims hold or not, and if so under what conditions, and that’s what today’s paper choice is all about. The authors give a formal and machine checked safety proof for a meaningful subset of Rust. If a library uses unsafe features, this gives a framework to say what verification condition it must satisfy for it to be considered a safe extension to the language.
Now be warned, this is not an easy paper (it’s POPL, we should expect nothing less – I like to imagine the PC have an ‘intellectual intimidation’ criteria in the review process, and no paper falling below a certain threshold can be accepted!). And even though it runs to 34 pages, you’d really need to consult the even longer technical report to fully understand everything. Fortunately for most of us it suffices to know that the work exists, the results it demonstrates, and the implications for Rust. So those are the aspects I’ll focus on today.