I read the OP differently. Type-level programming (not to be confused with type-oriented programming) is using the typechecker to perform computation on types,

I read the OP differently. Type-level programming (not to be confused with type-oriented programming) is using the typechecker to perform computation on types, which proves guarantees at compiler time. In this case, types are less about documentation, they are literally proofs of properties of the program by construction. In fact, type-level programming is usually unreadable[0] unless the reader has deep knowledge of the specific language implementation of type families, functional dependencies, poly-kinds, etc (whatever permits typelevel programming in that language). I'm getting that the OP is arguing against these ad-hoc constructs (type families etc) and would much rather write these proofs in the same language as ordinary code (e.g. writing the law "List x where length(x) == 5" in the type rather than "forall a. List (S (S (S (S (S Z))))) a") which, well who can disagree? In a sense, you and OP both agree on the same thing. Types are good. No types (or unreadable ad-hoc constructs for types) are not good. [0]: https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview uses type-level programming in Haskell to solve N-queens