4 ms·
This is about verifying the compiler, not proving any properties of the generated code. Totally orthogonal to Rust's aims, unless the Rust compiler has been for
by wk_end 8y ago
This is about verifying the compiler, not proving any properties of the generated code. Totally orthogonal to Rust's aims, unless the Rust compiler has been formally verified (I don't believe it has).
- steveklabnik 8y agoIt has not.
- strangecasts 8y agoThere has been work to verify a subset of Rust's logic - https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/ - but the compiler itself is not verified, no.