> I guess that immutable Rust is simpler to verify with the other systems too. I don't think that's the case (it's not harder either). The type system of Rust

> I guess that immutable Rust is simpler to verify with the other systems too. I don't think that's the case (it's not harder either). The type system of Rust makes handling mutability fairly trivial in verification, in fact it could be translated to immutable code in a continuation monad like the Tardis monad from Haskell I think.