Guy Steele on formal proofs from Coders at Work
Seibel: Do you ever try to formally prove your code correct?
Steele: Well, it depends on the code. If I’m writing code with some kind of tricky mathematical invariant I will go for a proof. I wouldn’t dream of writing a sorting routine without constructing some kind of invariant and proving it.
Seibel: Peter van der Linden in his book Expert C Programming has a sort of dismissive chapter about proofs in which he shows a proof of something, but then, ha ha, this proof has a bug in it.
Steele: Yes, indeed. Proofs can also have bugs.