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.
So you think the key for understanding constructive logic is to understand some peculiar syntax for a fragment of it. Ridiculous, but sadly quite typical among type theory cultists.
No one is saying type theory is useless, particularly when it comes to computation. It works within its own boundaries, but it does indeed have boundaries. There is a reason the ZFC has triumphed in mathematics.
Not really. The boundaries of type theory (say HoTT) are exactly what is possible on a Turing machine (computable). And a step beyond those throws ZFC itself into paradoxes (say Russel's). Moreover ZFC is directly expressible in type theory https://hott.github.io/book/nightly/hott-online-1174-g29279f...
I agree regarding the completeness of type theory in regards to Turing computability.
But I disagree regarding paradoxes in ZFC. Russel's paradox specifically applies to naive (simple Cantor) set theory, something the ZFC was explicitly designed to address with its axioms of choice and infinity. Furthermore the HoTT is itself expressible in the common extension of ZFC which adds at least one inaccessible cardinal.
And, mathematically speaking, the ZFC excels in dealing with infinities, which is more difficult (though possible) in the various type theories.
I agree with everything besides your stated difficulties with infinities in type theory. Here's one infinity
inductive ℕ : Type
| zero : ℕ
| succ (n : ℕ) : ℕ
the type of natural numbers with cardinality ℵ₀. Here' s a bigger infinity:
ℕ → ℕ
the type of functions over natural numbers.
From then on one can start talking about different injective functions between those types and infer cardinality of which is bigger and so forth and so forth.
It's values, types and functions all the way down. Nothing from ZFC is lost, on the bright side, your proofs are checked by a computer. On an even brighter side, your proofs can be semi-automated, even brute forced.
