Comment by jnwatson

And types can’t represent the properties shown by tests. Type checking as typically applied only catches the simple problems of feeding the wrong argument into a function.

Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance.