1. No type inference (unlike ML-style types).
2. Oracle problem: In practise you never have full specifications (let me be
provocative: Facebook has no specification in principle, only its ever changing code), and often,
especially in early phases you rarely have specifications.
3. You pay the price for dependent types always (e.g. having to prove
termination), even if you don't use interesting specifications.
4. Like Java's exception specifications, dependent types are 'non
local', meaning that a change in one part of the code may ripple
through the entire code bases, this stands in the way of quick code
evolution, which is important -- at least in early parts of
large-scale software projects.
5. Despite dependent types being 1/2 century old by now, and despite intensive effort, dependent
types have not really been successfully been generalised to other
forms of computing (OO, stateful, concurrecy, parallel, distributed,
timed) -- unlike competing approaches.
Summary: dependent types are wonderful as a foundations of
mathematics, but have failed to live up to their promise as general
purpose languages.
2. Oracle problem: In practise you never have full specifications (let me be provocative: Facebook has no specification in principle, only its ever changing code), and often, especially in early phases you rarely have specifications.
3. You pay the price for dependent types always (e.g. having to prove termination), even if you don't use interesting specifications.
4. Like Java's exception specifications, dependent types are 'non local', meaning that a change in one part of the code may ripple through the entire code bases, this stands in the way of quick code evolution, which is important -- at least in early parts of large-scale software projects.
5. Despite dependent types being 1/2 century old by now, and despite intensive effort, dependent types have not really been successfully been generalised to other forms of computing (OO, stateful, concurrecy, parallel, distributed, timed) -- unlike competing approaches.
Summary: dependent types are wonderful as a foundations of mathematics, but have failed to live up to their promise as general purpose languages.