Thanks. So what does it mean for a program to be memory safe if it can still memory leak? An example or pointing to a resource for further reading would be much appreciated.
It prevents data races, use-after-free, double-free, buffer overflow, invalid type punning, etc. You can still do all those things in unsafe code though, and you could in safe code if the unsafe code you depend on (including the kernel) behave/are programmed incorrectly. You can also have hardware issues and stochastic bit flips that Rust and SPARK can't deal with.
That’s not correct. Memory safety consists of properties necessary for type safety to be upheld. Leaks alone can crash a program but can’t defeat type safety.
Memory leaks in all languages are safe, they just slow performance and cause crashes.
Rust still memory leaks.