[geofft]

Types are tests.

In a sufficiently strong type system, you can express constraints stronger than "returns a string" or "takes an integer". For instance, if you want to make sure that a particular function always returns a valid file descriptor, make a structure for file descriptors that just contains a single int, and give it a private constructor that can only be called by the low-level functions that call the actual syscalls, or maybe a public constructor that confirms that the provided integer is actually a file descriptor. Then, as long as your function typechecks, it can only possibly return a valid file descriptor, for all possible inputs.

If you take this to an extreme, you get the https://en.wikipedia.org/wiki/Curry-Howard_correspondence, that there's a direct mapping between mathematical propositions and types, and between their proofs and functions of the corresponding type. This is what all modern proof assistants build on top of, though their type systems are usually extremely complicated.

[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.

[echelon]

Moreover, types are tests you don't have to write and maintain.