[impossiblefork]

Yes, but remember that Erlang bug discussed here last week where somebody apparently messed up SSH state transitions in such a way that people could just log in without having the password or anything?

Buffer overflows etc. are absurd things that should not be possible, but preventing them is the first step towards security.

[worldsavior]

This is something that Rust should prevent, not another layer on top of Rust.

[trealira]

Buffer overflow vulnerabilities are prevented with bounds checking, but that just means you get a panic at runtime. With formal verification, you can prove that the program never accesses an array with an index that's out of bounds.

I guess you're asking why that wasn't built into Rust from the start; after all, there are programming languages with the formal verification and theorem-proving built-in, e.g. for imperative languages, the SPARK extension to Ada, as well as ATS, or for a functional one, Idris. My guess is that Rust never would have become popular if you needed to write actual formal proofs to guarantee some degree of safety, since satisfying the borrow checker is easier in comparison, and it also probably would have been a lot harder to develop Rust after that. The borrow checker simply eliminating use-after-free errors and data races in safe code was good enough.

[impossiblefork]

Yes, it should make sure that there are not buffer overflows, but this is the next step.