You will never be able to get both 100% guaranteed memory safety and low level control/performance. Opposing it based on principle means that you'll never move on to anything better because a perfect solution doesn't exist.

For what it's worth, you can write quite a lot in 100% safe code, such that you have to trust only the standard library. Which is the case for any programming language.

So, the argument on the front page is true. It does guarantee memory safety in safe Rust code, as much as possible. It gives you the tools to extend your abstractions with unsafe Rust code, which you need to supply your own guarantees with.

> You will never be able to get both 100% guaranteed memory safety and low level control/performance.

Sure you can. You just need a full fledged proof engine instead of "merely" a type system.

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/