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&#x27;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.<p>Really good type systems are incredibly powerful tools for testing and refactoring code.