I just discovered, via CNN, that the Commodore 64 turned 25 last summer.

People that have met me later in life may be surprised to learn that I spent long hours programming for fun. Not that I need to be defensive or anything, and I certainly did not know so then, but, at the time, programming, even in the very basic Basic that came with the computer, was the closest thing I could do to math. Certainly, it was much closer than the “math” I was getting in school, which consisted in learning how to run certain numerical and algebraic algorithms by hand. Indeed I don’t think I encountered anything closer to math than programming until the first year of college, when the whole notion of axioms, theorems, proofs, and “playing a game with meaningless symbols” was unloaded on me in a course innocuously termed “Geometry.” (Nominally a course on linear algebra, the course was a parody of Bourbakism as a teaching style. In the first class the professor came in and said, a vector space is a set with two operations that satisfy the following nine axioms. Now I should like to prove the following proposition… I am not joking when I say that the fact that the elements of a $k$-dimensional vector space are $k$-tuples of numbers came as a revelation near the very end of the course.)
implementation of a program is similar to a proof should be familiar to anybody who has written both. In both cases, one needs to break down an idea into basic steps, be very precise about how each step is realized, if a sequence of steps is repeated twice in a similar way one should abstract the similarity, write the abstracted version separately, and then use the abstracted version twice, and so on. The Curry-Howard isomorphism establishes this connection in a formal way, between a certain way of writing proof (say, Gentzen proof system with no cut in intuitionistic logic) and a certain way of writing programs (say, typed $\lambda$-calculus). I know because I once took a course based on the totally awesome book Proofs and Types by Girard, which is out of print but available for free on the web.