Perhaps I'm missing something due to having read through the article too quickly. Please educate me.

The point I got out of this fine article is that we are under/misusing types.

Types encode logical propositions. The compiler, besides producing binary code, is also a proof checker. We should let it help us reason about the program instead of trying to do everything informally in our heads.