https://research.googleblog.com/2006/06/extra-extra-read-all...
Yes, you can asymptotically approach correct with testing, but it turns out that surprises can lurk for quite a long time if that's your approach. Of course, that's how most collections code works and what most of the world is built on, so yes, it is generally "good enough", but it is still worth pointing out that it is not necessarily correct, even after being out in the field for decades.
> I was shocked to learn that the binary search program that Bentley proved correct and subsequently tested in Chapter 5 of Programming Pearls contains a bug.
Rust does a great job of error checking in the 99% case and the 1% of unsafe should be from well vetted libs. No different than trusting the kernel to do the right thing.
On the other hand, collections are embarassingly testable. It's never been clear to me that formal methods gain much over thorough fuzzing/unit testing in this context.
(rust's testing falls a fair bit short of thorough unfortunately and there have been a handful of mem safety errors in their impls. although I'm not aware of this ever leading to an exploit in an application. mostly caught quite early with the release trains as a buffer)