Comment by stevenhuang
10 hours ago
So it moves from both "my implementation and specification is incorrect", to just "my specification is incorrect".
I don't understand this type of thinking. Proving what you can is still better. Don't let perfect be the enemy of good.
>> 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.