Since tomp objects to trusting code, then I agree with Manishearth: if you're never willing to trust code, then you can never have guarantees. Even the proof engine is trusted code.

Well, you have to trust something... Silicone manufacturer, CPU designer, the OS, the compiler...

But the big difference is, if I can do proofs and the compiler breaks my trust, that's a bug in the compiler. On the orher hand, Rust disallows complex proofs entirely, so I have to use unsafe code and trust random humans!

The compiler is just as much written by random humans as anything else.

This. There's no reason the smaller bits of `unsafe` code couldn't be verified with a proof system (ala COQ). Very few systems can be completely `true` in a mathematical sense, including math itself. IMHO, this is a self-defeating argument. E.g. a form of: "math isn't provable so math sucks!".

In the long run, this viewpoint would prevent moving to a system with 5% unsafe/95% safe which could be much more readily proofed using COQ since only a handful of unsafe code needs to be analyzed – I'm assuming proofing code has exponential complexity growth. So basically give Rust 10 years and I bet someone could build a verified stdlib & compiler for Rust!

This is already being worked on http://plv.mpi-sws.org/rustbelt/

Fantastic! Rust keeps getting better... Didn't realize Max Planck institute had a software division. Are you familiar with the state of their progress? I've been wondering when/how people might start applying monads to analyze shared imperative state. It appears to be somewhat of the approach in `Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning` paper listed. Going to have to keep an eye on these folks.

Well, ok. I guess that's too heavyweight, though.

However, http://plv.mpi-sws.org/rustbelt/