5 ms·
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
by grumdan 7y ago
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.
- dmitriid 7y agoTypes 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>.