After enough internalization, enough transformation, enough generalization, enough use, and enough connection, the mathematical community eventually decides that the central concepts in the original theorem, now perhaps greatly changed, have an ultimate stability. If the various proofs feel right and the results are examined from enough angles, then the truth of the theorem is eventually considered to be established. The theorem is thought to be true in the classical sense—that is, in the sense that it could be demonstrated by formal, deductive logic, although for almost all theorems no such deduction ever took place or ever will.
Mathematicians use simplicity as the first test for a proof
It must go through social processing to gain validity. And complex deductions can be harder to validate because of their length and minutia. If a proof cannot be read, its truth does not function as knowledge. A verifier would be the gold standard, but for sufficiently complex systems, such verifiers do not exist in practice.
Since the requirement for a program is informal and the program is formal, there must be a transition, and the transition itself must necessarily be informal.
Moreover, the specification itself evolves through the labor of implementation. Coding shapes the spec just as much as the spec shapes the code.
“Babysitting for a sleeping child for one hour does not scale up to raising a family of ten—the problems are essentially, fundamentally different.”
This echos a common insight (Mythical Man Month, etc.) that processes scale non-linearly.