Comment by steveklabnik

3 months ago

… except that Rust’s compiler has been qualified for several safety critical standards, with more to come, and has several formal verification tools as well. Amazon even has placed bounties (and paid some) for proving things about the standard library.

Rust is not as immature or evolving in the ways you imply.

8 comments

steveklabnik

Reply
johnisgood  3 months ago

Why would Rust need formal verification tools like https://github.com/rust-lang/miri if the programming language is so safe that it prevents them[1]?!

[1] Undefined Behaviors.

  • steveklabnik  3 months ago

    Miri is not really a formal verification tool. It is more of a runtime sanitizer.

    And it's because Rust's "no undefined behavior" is for safe Rust. Miri is used dynamically at runtime to catch undefined behavior in the unsafe superset.

    Finally, Rust's safety guarantees relate to memory safety only. There's a lot more properties you'd want to prove about programs, some safety related in a broader sense, some totally unrelated to safety concerns.