It's not a bad thing that Rust addresses these issues. That's good, and essential for newer languages---it wouldn't make sense to not try to solve these proble

It's not a bad thing that Rust addresses these issues. That's good, and essential for newer languages---it wouldn't make sense to not try to solve these problems in a language that intends to be lower-level (like Rust), relatively speaking. The paper on the Limits of Correctness that I mentioned above does a good job at arguing my point. Even if you rewrote glibc in a language like Coq and formally proved its correctness, that doesn't mean that it's "correct" in the sense that its logic mimics glibc---there could be logic errors. So you might gain confidence (or guarantees) in rewriting glibc in Rust, but in rewriting it you potentially introduce a host of new issues.