Rich Types?

Shin (weird for me to call this name!) repeated Lennart Augustsson's DTP '08 talk Can Dependently Typed Programming Succeed in the first MFN meeting this afternoon. Lennart presented the talk in a humorous style, which I enjoyed a lot. On p.14 of the slides, he mentioned that

Design Decisions

• Types must not be infested by extra predicates.
  • subtypes?
  • external vs internal logic.
• The same code can have many types (depending on used properties)
  • sort :: (xs :: List a) -> { ys :: List a; Perm(xs, ys); Ordered(ys) }
  • sort :: List a -> List a
  • sort :: (xs :: List a) -> { ys :: List a; Ordered(ys) }

I think issues like this can all be easily solved with externalism. Principles of software engineering keep telling us the importance of decoupling and how it leads to modularity and reusability, while indexed datatypes and annotated return types obviously introduce strong coupling. If some form of externalism is adopted, we don't get long, long types infested with predicates; we don't need many types for sort; we don't write multiple versions of one datatype that are indexed differently; change of specification simply means taking a different set of separate small proofs (if the code is not modified); proof erasure seems to be within reach; ...

So is there really a situation where indexed datatypes and annotated return types are necessary or a lot more suitable? Or is it because we just want to do indexed types and such, so we can call it dependently typed programming?

--
Or is it because I am not experienced enough?