> So you haven't understood the distinction or you're letting your feelings for software get the best of you.

Maybe? I'm not sure.

> The proof that there are no (for rust's definition of "no") memory bugs becomes worthless

I still don't think so, the proof that there are no memory bugs is definitely not worthless, since while the whole proof itself is binary (it is either fully correct or not), its effects act more like coverage, and the more of it that happens to be partially correct, the better.

I think cve-rs is the perfect example of this. Its very existence proves that the borrow checker is already unsound, and with that, the very foundations of Rust's safety guarantees are currently flawed.

TypeScript is another good example, its type system has been repeatedly proven to be unsound, so it's also flawed.

But so what if it's flawed? Many smaller properties of these proofs still happen to hold, and they might prevent 90%+ of CVEs even as flawed as they are.