Indeed, that’s why Dan North, Liz Keogh, et al have been banging the requirements capture drum for the last ten/twenty years.

Doesn’t mean it might not be useful.

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

That's the same logic as not writing tests because your tests might have bugs in.