Foundational, twice over. The λ-calculus is a rigorous, complete model of computation, and Church's theorem (first-order logic is undecidable, 1936) is airtight — together they fix the boundary of the mechanical alongside Turing.
Equivalence is provable; the thesis isn't. λ-calculus and Turing machines compute the same functions — that's a theorem. But the Church–Turing thesis (this is all effective computation) concerns an informal notion and can't be formally proved.
Two authors, one result. Church proved logic undecidable just before Turing, but Turing's machine was so vivid it took the public credit. The abstract λ-calculus was underappreciated for decades — then computing caught up to it.
Watch the calculus build the world from nothing. A boolean is just a chooser: TRUE = λx.λy.x (take the first), FALSE = λx.λy.y (take the second). A number n is "apply f, n times": 2 = λf.λx.f(f x). Define AND, OR, +, × as pure λ-terms, then beta-reduce — substitute and simplify — to a normal form. No primitives were used; only substitution. Each result below is computed live by an actual λ-evaluator.
map (λx → x+1) xs in any modern language, you are speaking Church's 1936 calculus directly; the λ keyword is his."The only thing that I have ever invented that has any importance is the λ-calculus — and I'm not sure even of that." — attributed to Alonzo Church
λ-calculus and the Turing machine compute exactly the same functions (proved 1936–37). Two utterly different pictures — substitution vs. a head on a tape — one notion of "computable."
Church's theorem: no algorithm decides whether an arbitrary first-order statement is valid. Hilbert's Entscheidungsproblem — "is there a procedure for all of logic?" — answered no.
That two minds, working independently with totally different tools, drew the same boundary in the same year is the strongest evidence for the Church–Turing thesis: that "effectively computable" has one robust meaning, captured equally by [[alan-turing]]'s machine and Church's λ. The machine became the hardware picture — the processors of PSĒPHOS; the λ-calculus became the software picture — the theory behind functional programming and the type systems descended from [[bertrand-russell]]. Same edge, two languages; the lineage of logic forks here into the two halves of computer science.
Gate kept on. The results are exact: the λ-calculus is a complete model of computation, its equivalence to Turing machines is a theorem, and the undecidability of first-order logic is proved. What stays a thesis is the philosophical claim that this captures all effective computation — overwhelmingly believed, supported by every model anyone has built collapsing to the same class, but not formally provable, because "effectively computable" is an intuitive notion, not a mathematical object. On credit: Church reached undecidability just ahead of Turing, but Turing's machine was so concrete that it, not the λ-calculus, became the popular image of computation — the abstraction waited decades for programming languages to make it obvious. The man was famous for monkish precision — he wrote in multiple colors of ink, erased rather than crossed out, and kept rigor near-religious — and he was a maker of makers: as a Princeton professor he advised Alan Turing's PhD, and also Stephen Kleene, J. B. Rosser, and others who built the field, founding and editing the Journal of Symbolic Logic for decades. The λ he set down in 1936 is, quietly, the most-used idea in this entire lineage that most people have never heard his name attached to. ⚑ With him the LOGIKĒ foundations rank closes: from [[thales-of-miletus]]' first proof to two equivalent definitions of the computable — the machine, and the function.