That's my understanding as well. The thing I was wondering as I read it: how difficult would it be for someone to make an extension or fork of Rust that allows

That's my understanding as well. The thing I was wondering as I read it: how difficult would it be for someone to make an extension or fork of Rust that allows annotating sufficient type information to prove these kinds of invariants, like F*?