This is one of the key ideas that Gödel, Escher, Bach tries to convey accessibly. I've always thought of it like a popular science book, but for logic. Unless y

This is one of the key ideas that Gödel, Escher, Bach tries to convey accessibly. I've always thought of it like a popular science book, but for logic. Unless you're already familiar with the ideas, it's a great place to start or even just get a taste. A great read for non-mathematicians. Viewing logic systems as objects themselves is a very important insight and yet surprisingly counter-intuitive. Logic is logic. It feels like the aether of reasoning--constant and ever-present. But in reality, you can easily design and use different systems with different constraints and philosophies, giving you different results. You can even reason logically about logic, considering a logic system as an object itself! I think this sort of realization is one of the most important steps to understanding that elusive "mathematical mindset" people like to talk about. For me, learning all about Curry-Howard and how programming relates to logic really opened my eyes. I'm already comfortable with treating programming languages and programs as objects--I do all sorts of metaprogramming and static analysis and so on. Seeing proofs and logic systems in the same light made everything clear. A proof is just a program; a logic just a programming language and so I can treat them in the same ways. I really believe Curry-Howard is one of the most important ideas I've ever learned--it gave me a new perspective on CS, a new perspective on mathematics and a way to naturally link the two. Thinking by analogy is very powerful, and Curry-Howard is ultimately just that, a rigorous analogy. As an aside, I think we can reasonably codify induction by talking about probabilities. See "Does Algorithmic Probability Solve the Problem of Induction"[1] which is a great paper that breaks Betteridge's law. (Sort of.) [1]: http://world.std.com/~rjs/isis96.pdf http://world.std.com/~rjs/isis96.pdf