Tony Morris

Statically typed languages are like having a spell checker AND a grammar checker up front. Dynamic languages mean I won’t know if I spelled anything wrong until I get my paper back from the teacher.

Unless, of course, you practice TDD. Then you know immediately because you are writing a very specific purpose spelling and grammar checker.

Tests are not proofs.

Neither are types.

Um. That’s exactly what they are. Perhaps you meant to say “types are only able to prove some things about your code, and I find that less useful than others do, but I see where you’re coming from”

The type is not the proof, it is the statement to be proven by a program. In any case, expressing all necessary behaviors as types is impractical; but as tests is trivial.

Further, using types appropriately, has the same practical outcome as writing infinity tests, but with zero effort and zero hindrance. Where is that trade-off exactly?

No, not even close. I can completely replace static types with tests. I cannot completely replace tests with static types.