6 ms·
Rust has a lot of nice safety features, but the compiler hasn't been formally verified at all.
by panic 9y ago
Rust has a lot of nice safety features, but the compiler hasn't been formally verified at all.
- steveklabnik 9y agoThis is true, but work is in progress, and some parts of the standard library already have been. And some of that work has found bugs too: https://github.com/rust-lang/rust/pull/41624 https://github.com/rust-lang/rust/pull/41624
- lazaroclapp 9y agoYeah, I am aware. The problem is that using, say, CompCert might result in less security in practice, since although the compiler transformations are verified, code written in C is usually more prone to security issues. It also puts the burden of proving memory safety on the developer, which is a requirement for proving nearly anything else. I don't know Rust well enough to know if this applies for sure, but I think it is a lot less to ask from the manufacturer that they produce a proof of the form "assuming this language's memory model holds, we have properties X, Y and Z" and then just hope the compiler is sane, versus requiring a more heavy-weight end to end proof. Also, eventually there might be a mode for certified compilation in Rust/Go, at which point you get the best of both worlds.