> A system that is not even Turing complete is extremely limited.

Agda is not Turing-complete, yet it is very useful.