Hacker News Reader

At least now we are checking that two pieces of saying what we want a program to do match up. It's less likely to get both the implementation and specification (in the form of types) wrong. Whenever the program fails to type-check, it will make you think about both bugs in the type and bugs in the code, even if the latter is more likely.

View on HN

Types can’t encode the specification fully, or require a lot of work to encode a specification (so most people will skip this work).

The simplest example is very common banking and e-commerce logic which is basically a series of checks in the form:

if <some piece of data retrieved at runtime at that particular moment> is consistent with <multiple other pieces whose number and relevance depends on that data retrieved at runtime from potentially multiple sources>.

Reply on news.ycombinator.com