[chriswarbo]

Sibling comments are talking about "good types need fewer tests, yada yada" which is somewhat subjective (although I happen to agree with it).

More objectively, a dependent type system (like Idris, Coq, Agda etc.) is a test framework, since it can run arbitrary code.

Instead of writing tests as booleans, with 'true' for pass and 'false' for fail, we write them as types, with the unit type for pass ('()' in Idris) and the empty type for fail ('Void' in Idris), e.g. see this thread https://news.ycombinator.com/item?id=24567404

Of course, we can do the usual monad/effect-system tricks to implement a 'throw TestFailException' API on top of that, if we prefer.