That is true in general. But 1. unsafe code in the standard library is of course more battle-tested than ad-hoc unsafe code, and 2. there are efforts to formall

That is true in general. But 1. unsafe code in the standard library is of course more battle-tested than ad-hoc unsafe code, and 2. there are efforts to formally verify Rust. http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/ and https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 https://internals.rust-lang.org/t/announcing-the-formal-veri...