> Rust is still a huge improvement
> Except that it's not guaranteed
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.
Sure you can. You just need a full fledged proof engine instead of "merely" a type system.
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!
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!
However, http://plv.mpi-sws.org/rustbelt/
This is a vast oversimplification.
It relies on you trusting tiny bits of unsafe code which have been carefully reviewed. This is opposed to entire C codebases which need reviewing. It's much, much easier to audit 10 lines of unsafe code than it is to audit an entire application.
The vast majority of Rust code is not unsafe.