> There are entire classes of considerations you can dispense with entirely due to how the Rust language works.

That sounds like it would still be necessary to standardize, specify and prove a lot about Rust and its compiler, to exploit those facets of Rusts' behaviour?