> Types are just human and machine readable documentation

This is only possibly true in the context of languages with poor static typing ecosystems, and even then I don't think I fully agree.

When a type-checker admits a program, it is because it has proved the program to be free from certain classes of errors. The more expressive your type system, the more elaborate and precise your claims about your program's behavior can be. This is fundamentally distinct from providing documentation that tells your users "please don't input values outside this range".

Early type systems (like C's) are woefully incapable of any serious specification. Modern type systems are significantly more expressive, and are therefore significantly more capable than you suggest. Types in the context of these expressive type systems are logical propositions, and the programs we write are their proofs.

Type theory has applications far beyond readable documentation. It is the basis for modern science.