Interesting. I would have thought that leak-free is part of the premise, since you can very well right C or C++ with a guarantee of no use after free at least, assuming you don't care about memory leaks.

The difference is that memory safety of any kind (including leaking everything) in C/C++ requires discipline, whereas in Rust the compiler is what prevents it. And yes, leaking is not part of that guarantee, because leaks cannot cause corruption or undefined behavior.

With that said, while Rust does not guarantee it, it does have much better automatic memory cleanup compared to C++, because every value has only one owner, and the owner automatically drops/destructs it at the end of its scope.

Getting leaks is possible to do with things like Box::leak, or ref-count cycles, but in practice it tends to be explicit, rather than the programmer forgetting to do something.

One of the reasons I was disappointed about Rust when it came out.

But preventing memory leaks is actually impossible. Even with garbage collection, memory leaks are common.

It’s certainly possible with appropriate proof methods. My disappointment was specifically about non-memory resources, however.