Tony Morris

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.

That's definitively not true. Want me to write the code for which you will never be able to write tests?

I’ve seen lots of code for which writing tests is nearly impossible. We call that legacy code. There are also behaviors that are not practically testable. E.g. fully testing the multiply operator.

Yes, you can practically fully test the multiplication operator. It's called a proof. It's exactly what types do.