Hacker News new | past | comments | ask | show | jobs | submit login

> 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.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact