Proving something correct is not a pancea either, although it can result in code that is generally "good enough". https://research.googleblog.com/2006/06/extra-extra-read-all...

> 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.