[drc0]

> That’s the equivalent of writing type annotations for programming functions. And the goal is avoiding bugs instead of logical contradictions.

mh, given Curry–Howard correspondence, aren't those the same? so the goal is indeed not having logical contradictions?

[Sharlin]

Yes. But it's a rare programmer, or even a programming language designer, who thinks of well-typed programs in terms of proving theorems.

[philix001]

They are. I avoided introducing an explanation of Curry-Howard isomorphism because I think that would not be very intuitive to many people because the most commonly used type systems have very little power to express logical properties about the program.

I may write another article about this.