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.