Recently Boats wrote a blog post about Rust, mutable aliasing, and the sad story of local reasoning over many decades of computer science. I recommend that post and agree with its main points! Go read it! But I also thought I’d add a little more detail to an area it’s less acutely focused on: formal methods / formal verification.
TL;DR: support for local reasoning is a big factor in the ability to do automated reasoning about programs. Formal verification involves such reasoning. Rust supports it better than many other imperative systems languages – even some impure functional ones! – and formal verification people are excited and building tools presently. This is not purely by accident, and is worth understanding as part of what makes Rust valuable beyond “it doesn’t need a GC”.
The rest of this post is just unpacking and giving details of one or more of the above assertions, which I’ll try to address in order of plausible interestingness to the present, but I will also throw in some history because I kinda can’t help myself.
The author is Graydon Hoare, the “founder” of Rust and technical lead until around 2013.
The other day I saw a link to Verus on here and it’s made me somewhat interested in the topic how Rust and formal verification can work together.
It’s quite insightful to see how the borrow checker both required and ended up facilitating the ability to do more extensive formal verification on Rust code.
Something like Verus (I haven’t looked into most of the other tools in this space yet, there seem to be many!) does appear poised to make verification quite approachable in low-level, self-contained Rust code already, and I’m curious to see how things evolve from there.
It would be exceedingly cool if one day there’s a subset of libraries on crates.io that are fully verified (similar to how today there’s a subset that supports
no-stddevelopment) and which are then usable to build upon in your own formally verified code.