| I'm probably not the best person to say what I'm about to say. In my university days, I took a graduate-level class called Software Foundations. We used Haskell to learn and implement type systems and a few other things. At the time I had no idea why it has "foundation" in the course title, because to me all of that was advanced stuff. Eventually, I had my moment of enlightenment, and it all became clear to me. These where infact theoretical underpinnings of software. Till then, I've only seen computation from the perspective of electricity->bits->circuits->...->assembly->the C language (and everything that comes above it). Over there, the "foundation" was bits and electronics using which you can make logic gates, develop the arithmetic & logic unit (ALU) and control unit, and build everything on top. On the other hand, with Lambda calculus, Church numerals etc I was approaching computation from the other direction — the mathematical perspective. It's also foundational, in that you can build up everything that you need — ALU and control unit — using Lambda calculus. Indeed it was eerie the first time I added on paper two Church numerals using Lamba calculus and the correct result popped out. Even though I knew the theory was sound — and I know this is a dumb thing to say — it was still so cool to see it work in practice. |