|
Better off, because I could have learnt the conventional axioms as a skill, like the perceptual and motor skills comprising reading, writing, arithmetic. And only later question them. My "optimism" is more for my intuition; working code is experimental confirmation. It's easier to be optimistic about code than proofs. Firstly, working code only needs to work in the specific cases you're using (that you test for); but a proof must work in every possible case. Thus, working code is simpler and easier to check, because it's aiming at less. My code almost always confirms my intuition. Yes, it's also helpful to have the automatic, mechanical check of executable code; and as you say, this relies on compilers, OSes, silicon, hardware. (Though, anecdotally, I have noticed subtle problems that I eventually diagnosed and confirmed to be compiler and hardware bugs.) BTW, yes I have tried COQ (proof assistant; somewhat mechanical proof checking), but simple ideas become very complex to prove, and the problem of bugs in COQ itself etc is of greater concern, for the next reason: Secondly, and relatedly, is that the standard is much lower for code. It just needs to work. Whereas a mathematical proof is supposed to be absolutely true. In other words, I don't ask as much from code. If there turns out to be a bug, it's just learning more about the problem; about the world. It's an engineering flaw.
But if my proof is wrong, the game is lost. An argument against my intuition is probably more telling. Though my faith in it has turned out to be justified many many times, I certainly can be wrong. My only real excuse is that, as a human being, I have nothing else to fall back on but my sense of reality and reason. That's my hardware; if it's wrong, I really am lost. So I might as well trust it.
Fortunately, it's almost always right; probably because I try to see things from many angles and check them in many ways before my intutive sense is fully formed. |