[actsasbuffoon]

I completely agree. For example, dependent typing lets you create a CSV type which ensures that each row added has the same number of columns. All of this is checked AT COMPILE TIME! The best part is that it's actually easy to do. Within a day or two of looking at Idris I could figure out how to build the previously mentioned CSV type.

Really good type systems are incredibly powerful tools for testing and refactoring code.