[hiker]

https://en.wikipedia.org/wiki/History_of_type_theory

Not that much surprised. History of type theory is a history of trying to define precisely computation. That is, try to allow recursion but enforce that all programs terminate.

The solution to this problem these days is to use a purely functional programming language with dependent types (e.g. Homotopy Type Theory, Lean).

Haskell, for example, being a practical functional programming language, is logically inconsistent. Using the fix function:

  fix :: (a -> a) -> a
  fix f = let x = f x in x

one can produce proof of everything

  Prelude Data.Function> :t fix id
  fix id :: a

that is just an infinite loop.

In a logically consistent functional language such as Lean https://leanprover.github.io, this definition is not allowed.