Comment by nullc

> but it could just as well be ported to Rust

Without formal semantics for the complete rust language the result couldn't be verified. Rust's complexity makes it hard to define formal semantics.

I wouldn't normally bring this up as a disadvantage of rust, but people aren't normally talking about software that has been formally verified.