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.