> A formal proof has value, but it's certainly not an absolute - relying on it blindly to indicate the correctness of a program is putting yourself at risk. In

> A formal proof has value, but it's certainly not an absolute - relying on it blindly to indicate the correctness of a program is putting yourself at risk. Indeed, I agree, but lots of people never ask themselves how much more at risk they are putting themselves when their implementation has no formal spec or proof at all! Like another commenter has argued, it seems that people seem to look at formal verification like it's an all-or-nothing approach (either it achieves zero bugs or it's completely worthless, or alternatively -- if it's formally verified then it MUST be bug free!), but it's really not, it simply gives higher (often, much much higher) assurances.