| A little bit of historical background. There was a concerted effort in the late 19th, early 20th century (perhaps earlier too) to mechanise computation i.e., reducing it to a pure symbolic manipulation. There were obvious benefits, a famous one being Enigma Machine that was used to (successfully I think) break the German code during WW-2. On the philosophical side a parallel and overlapping effort was going on to figure out if mathematics could represent all possible truths, again as symbolic manipulation system. Bertrand Russel's magnum opus Principia Mathematica [1] was one such famous work towards it. Kurt Gödel then made a breakthrough when he proved that such a system is impossible; i.e., a system can either capture all the truths or it can be consistent but not both[2]. Put differently, any mathematical system capable of representing all the truths will necessarily contain contradictions within it. Now coming to your question. Lambda calculus emerged in this milieu. Alonzo Church[3] invented one such system to mechanise computation, named ƛ-calculus. Using this system one can mechanically compute any function purely by symbolic manipulation. Later on Turing, Church's student I think, invented a totally different system named Turing Machine with the same purpose. Later on it was proved (by Church and Turing I think, but I'm not 100% sure) that ƛ-Calculus and Turing Machine are equivalent, Church-Turing thesis[4]. All these work, and more, laid the theoretical foundation for the modern computers. If we can today safely assume that computers are provably correct it's because of them. Phil Wadler has an absolutely delightful talk where he takes us through a whirlwind tour of the history of the mathematical foundation of computers [5], highly recommended. [1] https://en.wikipedia.org/wiki/Principia_Mathematica [2]https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor... [3] https://en.wikipedia.org/wiki/Alonzo_Church [4] https://en.wikipedia.org/wiki/Church–Turing_thesis [5] https://www.youtube.com/watch?v=IOiZatlZtGU |