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