The first principles of computation are not the first principles of software development. A computer is not a Turing Machine: it is an electro-mechanical wrappe

The first principles of computation are not the first principles of software development. A computer is not a Turing Machine: it is an electro-mechanical wrapper around the limited imitation of a Turing-like core, and that wrapper and the physical properties of the system put extreme limitations on what can or cannot be proven. Software development is a perfectly ordinary engineering activity, or should be (although it is mostly done by non-engineers), and the same standards should apply. No mechanical engineer or electrical engineer has ever shipped a "provably correct" machine. They have shipped machines that conform to best practices, including heuristic analyses of MTBF and so on.