>Let me clarify my position: In theory yes, you're right, it is decidable. In practice Agda and Coq force you to prove pretty much everything about your program using expensive annotations, in order to satisfy the typechecker. It's like pulling teeth. The type checker must be taught that your program terminates, and it must be taught that you maintain even the most simple of invariants.

That's why we need gradual typing. Some critical parts should be written with full dependent types with termination checker, etc, but most of the code should be just type checked.

P.S. I have some dependent types experience, including applying Coq in commercial projects.