Here's a small attempted answer: Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Even some programs that may conve

Here's a small attempted answer: Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Even some programs that may converge have no type. The Y Combinator, for instance, has no type because it would require an infinite type. From the Wikipedia article under "General Observations": Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a λ abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = (λx.x x) (λx.x x) . Recursion can be added to the language by either having a special operator fixₐ of type (α → α) → α or adding general recursive types, though both eliminate strong normalization. Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it always halts. We can therefore conclude that the language is not Turing complete. Another way to look at it is this via the Curry-Howard correspondence [^2]: for any mathematical proof, you can write down a program that is equivalent to that proof. Verifying the proof's result is the same as running the program. This is a very exciting correspondence that runs deep throughout computer science and mathematics. (I highly recommend the Software Foundations course I linked to below.) Writing a non-terminating program is like writing one of these self-contradictory logic statements: it has no proof of truth or falsehood. Thus, the fact that we can write programs to which we can assign some kind of type but that never terminate is a way of demonstrating the fact that there are theorems that are well-formed but have no truth assignment to them. (Gödel's Incompleteness Theorem) [^1]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; see also https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... [^2]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...