[dmitriid]

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