"It is by logic we prove, it is by intuition that we invent" - Henri Poincaré I emphasized the invention, but you're quite right that we also need the proving.

"It is by logic we prove, it is by intuition that we invent" - Henri Poincaré I emphasized the invention, but you're quite right that we also need the proving. I agree with your hardware example (things like the Pentium bug are rare...), but I think we similarly rely on other layers (OS, languages, libraries), though I concede with eroding confidence as we rise. For hardware, it's also that we have more trust in the common pathways (Dijkstra wouldn't like it - it all should be perfect. I can relate to this, but that's not how it is - today, anyway). Popular hardware is used extensively, and very importantly, I think it tends to be designed to be pretty flat, in that almost all of it gets exercised by almost all uses (i.e. there are few rare pathways). So flaws will show up quickly. We also don't worry about the language not correctly implementing a+b So I think you can make that assumption about code, if the code is well exercised (e.g. in a fundamental part of the code in the language runtime). Concessions: Dr. Gosling apparently did write some (informal) proofs for Java, but it was in the byte-code verifier, not for the typical language stuff. But I've heard that Intel does some formal verification :-). I agree that formal analysis is a worthwhile endeavour. I just wish they would do more work on interesting, useful problems. It used to be that computer scientists would invent something incredibly cool (like Boyer-Moore substring matching, or arithmetic coding), and then also prove it (well, really, prove some specific qualities about it). But these days, there seems to be a lot of proving things just because they can be proven - not because they are worthwhile proving. It's quite... insular. They focus on proof, not invention.