The Amazon.com front page generating code is a proof relating some properties of its output to its input and that it halts. However it's also basically incompre

The Amazon.com front page generating code is a proof relating some properties of its output to its input and that it halts. However it's also basically incomprehensible, so I doubt anyone alive could actually tell you precisely what it's proving. Your ability to prove something in any language is dependent on having a formal semantic for that language, or at least for a cognitively manageable subset that you're willing to restrict yourself to. The language semantics and memory model serve as axioms. Given how American programmers are trained, it's not realistic to expect them to be able to think of programs in a logical semantic way. There is something of an art to it and it's hard to learn a new way of thinking when you're satisfied with a way you already have. I agree that you can have an enjoyable hobby or make a living programming without really understanding what you're doing beyond intuitively and that's totally fine. Computing time is cheap and most applications don't cause any great harm when they behave in unintended ways. However the isomorphism between predicate calculus and computer programming isn't subjective. Programs really are proofs, just some of them are very sloppy.