Turing Completeness Is Overrated: and here's why
summary
Argues that Turing completeness is overvalued because untyped lambda calculus plus the Y combinator produces logical inconsistency, while adding types (simply typed lambda calculus) forces termination and consistency. Points to the 1930s equivalence of recursive functions, lambda calculus and Turing machines, and the Curry-Howard correspondence that treats function signatures as logical propositions. Claims sub‑Turing languages still support structural recursion, list comprehensions, parsers, state machines and config/query DSLs, and warns against accidental Turing completeness.
AI-written summary · about
chapters (5)
- 0:00Start
- 0:16Turing Completeness Is Overrated
- 2:05Prove that Recursive Functions from Girdle and Untyped Lambda Calculus and Turing Machines Are All Equivalent
- 3:16Functions and Logical Implication
- 5:22Accidental Turing Completeness
related talks
19mIll-Typed Programs Don't Evaluate
48mA History of Subtyping
30mA Complementary Approach to Incorrectness Typing
30mLambda Calculus: The Origins of Functional Programming
52mType Theory and its Meaning Explanations
30mContinuations and Coexponentials
42mWould Aliens Understand Lambda Calculus
48mWeird Machines: Exploiting Turing-Completeness