This is why correctness-oriented programming methods, while popular among academics, have and always will struggle with mainstream adoption.
A corollary of Tog's Paradox is that the definition of "correct" in a given program is always changing (as requirements evolve).
There are exceptions, like rocket science.