Programs are Proofs

The Howard-Lambek-Curry Correspondence gives a three way isomorphism between a typed lambda calculus, some intuitionistic logic(the logic of constructionist mathematics), and a cartisian closed category. One of the implications here is that programs are proofs and what they prove is the preposition that their type corresponds to. I've been reading about all of these systems trying to get a deeper understanding of what is going on here, and I've just realized something that, while probably obvious, has really put these things together for me.

Any term in the lambda calculus can be described by 1. variables 2. applications 3. abstractions. This means that any term can be broken down into pieces that are in turn one of those three cases. The most common way to prove things in this system is by induction on the structure of a term.

In Haskell, we have the hugely useful pattern matching mechanism. Until now I thought of it only as a nice way to take apart things defined by algebraic data types and give case analysis. But of course this is exactly induction on a data structure, meaning that the function that does this matching is proving a property of the structure by showing it for the base cases and handling the recursive cases by structural induction. Not only are programs proofs, they can have the same form as a proof! Clearly the type of the function is a statement which the function is a proof of!

One of the cool things about this is that it makes it much more clear (to me) that not only are programs proofs, but proofs are programs. In constructionist math all proofs must actually construct they thing they are proving and are therefore algorithms. This is really inspiring me to read up on constructionist math, and for reference a good blog about this is:http://math.andrej.com/