> In 1960, John McCarthy published a remarkable paper in which he did for programming something like what Euclid did for geometry.
One could argue that Church's (1930s) lambda calculus, which underlies LISP, is a closer analogue to Euclid's distillation of the essence of Geometry.
With the minimal addition of pure binary IO, the lambda calculus is easily transformed into an untyped programming language [1]. On the other hand, full blown and richly typed pure functional programming languages like Haskell remain semantically faithful to their lambda calculus underpinnings.
lambda calculus was a tool, but it seems godel and turing's work on computing machines and recursive functions were more fundamental to the original lisp.
The claim seems accurate to me, at least for Scheme: that is, lambda calculus does underlie Scheme.
Lambda calculus, as articulated in Church's 1935 paper, gives us a way to understand computability. But if we look specifically at Operation II in the paper (p. 347), what we have is the lambda function in Scheme. Given that every function in Scheme (including special forms) is equivalent to some lambda function, it seems that in virtue of Operation II we can say that lambda calculus underlies Scheme.
Whether we can push this further to say that lambda calculus underlies McCarthy's initial conception of LISP, or some arbitrary version of Common Lisp, I do not know for certain. But if all these versions treat lambda functions the same way as Scheme does (in relevant respects), then the claim holds for Lisp generally.
[1]: Church. An Unsolvable Problem of Elementary Number Theory. _American Journal of Mathematics_, Vol. 58, No. 2. (Apr., 1936), pp. 345-363.
One could argue that Church's (1930s) lambda calculus, which underlies LISP, is a closer analogue to Euclid's distillation of the essence of Geometry.
With the minimal addition of pure binary IO, the lambda calculus is easily transformed into an untyped programming language [1]. On the other hand, full blown and richly typed pure functional programming languages like Haskell remain semantically faithful to their lambda calculus underpinnings.
[1] https://tromp.github.io/cl/Binary_lambda_calculus.html