[cwzwarich]

With its current design trajectory, Rust won't be able to prove interesting high-level invariants. It's going to give you the kinds of things you can prove with traditional ML-style type systems and affine types. The combination of the two lets you encode some interesting things, e.g. typestates, but they won't let you express something like "this browser engine correctly implements CSS".