What are the limitations of dependent typing? It seems dependent types can provide lots of desirable guarantees about program behavior. What kinds of program properties can they NOT guarantee (besides what's computationally infeasible)? Is there an even more powerful or general type system that can model any computable property of a program?
One obvious missing feature from most dependent type theories is the ability for substructural reasoning.

The guarantees given by systems like Agda and Coq tend to be very extensional, that is they enforce properties about the values of the computations, rather than their operation. Some obvious things we might want to track about the operation of an algorithm:


Runtime
Space usage
Which resources they "own", e.g. which files they are allowed to access without risk of a race condition


All these things (and more!) become possible with various flavors of substructural types. This seems to be an important active research subject in the PL community.

A possible reference is Wadler, Linear Types can Change the World!

Note that using "deep embeddings", it is possible to enforce some of these properties in a standard dependent types system, see e.g. Brady &amp; Hammond Resource-safe Systems Programming with
Embedded Domain Specific Languages.