3 ms·
Rust, an immature language with fluidly evolving specification / reference implementation, is not suitable for high assurance nor formal verification.
by snvzz 11mo ago
Rust, an immature language with fluidly evolving specification / reference implementation, is not suitable for high assurance nor formal verification.
- steveklabnik 11mo 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.
- fooker 11mo ago> Amazon even has placed bounties (and paid some) for proving things about the standard library. Can you provide some links? Thanks.
- steveklabnik 11mo agohttps://aws.amazon.com/blogs/opensource/verify-the-safety-of-the-rust-standard-library/ https://aws.amazon.com/blogs/opensource/verify-the-safety-of...
- fooker 11mo agoThis is awesome. Are these reasonably current?
- steveklabnik 11mo agoThat announcement was a year ago, I haven’t kept up with the repo.
- johnisgood 11mo agoWhy would Rust need formal verification tools like https://github.com/rust-lang/miri https://github.com/rust-lang/miri if the programming language is so safe that it prevents them[1]?! [1] Undefined Behaviors.
- steveklabnik 11mo agoMiri 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.
- johnisgood 11mo agoIs it possible to find UB in "unsafe" at compile time?
- steveklabnik 11mo agoBy using some proof tools, you can find some of it. It is technically impossible to find 100% of it at compile time because some of the finer details about what is UB are not nailed down 100% yet. But those are generally pretty fine corner cases, and one of the goals of those definitions is to not invalidate code as written. Formal verification is very hard.