Tony Morris

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?

Of course some things are unprovable in any type system. And tests to prove trivial things are really irritating and unproductive to write. So it’s worth having a mix.

Sure. Sometimes. Bu the bottom line is that I can write good systems with tests and no static types. I cannot write good systems with static types and no tests.