No, Rust's argument is that it eliminates memory unsafety. It even says so on it's front page: "guaranteed memory safety".
Except that it's not guaranteed. It relies on you trusting code that (supposedly) expert programmers have written, and which has been reviewed hundreds of times. Which is no better than C.
I agree that this criticism is mostly a theoretical one; Rust is still a huge improvement (in safety, and probably other areas) over C. But some people (e.g. myself) oppose lies in principle, no matter how well-intentioned they are.
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.
> 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/
The only difference is that Rust 1) moved some of that into the stdlib and 2) lets third parties extend it to provide more guarantees.
Given this, I think you're drawing a rather arbitrary line- Rust (the compiler + stdlib, optionally + other libraries wrapping unsafe) does guarantee memory safety, full stop. Whether the guarantees are provided by the stdlib or compiler is irrelevant.
The argument has always been that it reduces the amount of code you have to check for safety manually. Most of it will be checked by the compiler. Have you run into the problem that most of your code is unsafe?
I've only started dabbling in Rust for some projects, but I've not had to write a single line of unsafe yet, and don't see where that would change.