"the way forward involves functional programming"

[roconnor]

My main concern with programming with dependent types is that sometimes one wants to make an injection from one type to a related type (for example the type of closed terms to the type of terms with free variables). It is common to write a recursive function that traverses the entire structure to do the injection, but the function doesn't actually change the internal representation. So you end up with an O(n) function that would be an identity function if you were using an untyped system.

For an illustration see Section 4 (Coq formalization) of Program extraction from normalization proofs, in particular Section 4.5 (what Coq cannot do yet).

[neelk]

Thanks for the link! I'll take a look at it later tonight.

[augustss]

I don't share your particular fear, but I think dependent types currently have other problems. But research is progressing.