Comment by jongjong

>> Don't let perfect be the enemy of good.

I feel like the exact same line could be used to argue the opposite point against formal verification.

I'm not saying that proof is inherently bad. If it was free, then I agree it would be good, but my point is that it's not free. Proofs are expensive to produce, maintain, they lock-down flawed implementations, focus on correctness but disregard more important aspects like modularity (I.e. loose coupling, high cohesion). Also; formal proofs discourage change and they create false confidence about reliability because sometimes the bug is in the spec itself, especially as the spec gets more complicated.

I think modularity is a more useful property to aim for in terms of achieving the right degree of correctness over the life of the software, in a practical sense.

Formal proofs can work against modularity if the proof must be rewritten in order to achieve modularity as requirements change over time; which is the reality for most software.