Tony Morris

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.

We can begin with that. I’d like to see that proof.

Well, I could write and show you the proof, but that itself won't be very helpful. Want to write a trivial proof ourselves first?