I took a programming course where we wrote a number of programs in assembly language. We were given a set of rules and operations, a starting point, a goal, an

I took a programming course where we wrote a number of programs in assembly language. We were given a set of rules and operations, a starting point, a goal, and we spent our time carefully assembling sequences of statements that took us from the starting point to the goal while obeying the rule system. I took a math course where we did a number of proofs in natural deduction. We were given a set of rules and operations, a starting point, a goal, and we spent our time carefully assembling sequences of statements that took us from the starting point to the goal while obeying the rule system. I'm dense, but I wondered about the strength of the correspondence between the two. It turns out that there's a nice paper by Philip Wadler [1] that illustrates the equivalence of natural deduction (math) and Church's lambda calculus (math, but programming). [1] 'Proofs are Programs: 19th Century Logic and 21st Century Computing', Philip Wadler