Dependent types can prove your code is correct up to a specification. But how do you prove the specification is correct?

Solution 1:

This is the static, type-system version of, How do you tell that your tests are correct?

The only answer I can honestly give is, yes, the more complex and unwieldy your specification, the more likely you are to have made a mistake. You can mess up in writing something in a type theoretic formalism just as well as you can in formalizing the description of your program as an executable function.

The hope is that your specification is simple and small enough to judge by examination, while your implementation of that might be far larger. It helps that, once you have some "seed" ideas formalized, you can show that the ideas derived from these are correct. From that point of view, the more readily you can mechanically and provably derive parts of your specification from simpler parts, and ultimately derive your implementation from your specification, the more likely you are to get a correct implementation.

But it can be unclear how to formalize something, which has the effect that either you might make a mistake in translating your ideas into the formalism – you might think you proved one thing, when actually you proved another – or you might find yourself doing type theory research in order to formalize an idea.

Solution 2:

This is a problem with any specification language (even English), not just dependent types. Your own post is a good example: it contains an informal specification of "sort function" that only requires the result to be sorted, which is not what you want (\xs -> [] would qualify). See e.g. this post from Twan van Laarhoven's blog.

Solution 3:

I think it's the other way around: a well-typed program can't prove nonsense (assuming the system is constistent), while specifications can be inconsistent or just silly. So it's not "how to make sure this piece of code reflects my platonic ideas?", but rather "how to make sure my ideas meaningfully project onto a well-founded plane of pure syntactic rules?". How to make sure the bird you see is a mockingbird [for some supplied notion of mockingbirdness]? Well, study birds and raise you chances to be right. But as always with humans, you can't be 100% sure.

Type theory is a way to mitigate the imperfectness of human mind by introducing formal rules, machine-checked proofs (it's a very relevant paper) and other stuff, that allows to focus and thus to simplify problems a lot (as Brouwer said: "Mathematics is nothing more, nothing less, than the exact part of our thinking"), but you can't expect any tool to make your thoughts "right", because there is just no uniform notion of rightness. IOW, there is no way to formally connect informal and formal: being informal is like being inside the IO monad — there is no escape.

So it's not "does this syntax reflects my very precise semantics?", but rather "can I attach my raw semantics to this strongly structured syntax?". Programs are proper material objects, while ideas are cumbersome approximations, that can become proper material objects only by convention. So we form some basis using conventions, and then we just trust it, because it's much more sensible to trust to a small subset of all your numerous ideas than to all of them.