Dependent types can confirm that your code conforms to the specification. But how do you prove the specification is correct?

Question

Dependent types are often touted as a way to give you the ability to claim that a program meets specifications. So, for example, you will be asked to write code that sorts the list — you can prove that the code is correct by encoding the concept of “sorting” as a type and writing a function like List a -> SortedList a . But how do you prove the correctness of the SortedList specification? Isn't it that the more complex your specification is, the more likely it is that your encoding of this specification as a type is wrong?

Answer 1

This is a static version of a system like How do you say your tests are correct?

The only answer I can honestly say is the more complex and cumbersome your specification, the more likely you are to make a mistake. You may be mistaken in writing something in a formal formalism of the type as good as you can in formalizing the description of your program as an executable function.

We hope that your specification is simple and small enough to judge by the exam, while your implementation can be much larger. This helps in the fact that once you have formalized “seed” ideas, you can show that the ideas derived from them are true. From this point of view, the more easily you can mechanically and provably obtain a part of your specification from simpler parts and ultimately extract your implementation from your specification, the more likely you are to get the correct implementation.

But it may not be clear how to formalize something that can lead to a mistake in translating your ideas into formalism - you may think that you proved one when you actually proved the other - or you can find yourself researching type theory so that formalize the idea.

Answer 2

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

Answer 3

I think the opposite is true: a well-typed program may not seem pointless (assuming the system is constant), while specifications can be inconsistent or just plain dumb. So this is not “how to make sure this piece of code reflects my platonic ideas?”, But rather “how to convince my ideas of significant progress in the substantiated plan of pure syntax rules?”. How to make sure that the bird you see is a mockingbird [for some ridiculous notion posed)? Well, study the birds and increase your chances of being right. But since it is always with people , you cannot be 100% sure.

Type theory is a way of mitigating the imperfections of the human mind by introducing formal rules verified by a machine of evidence (this is a very relevant article) and other materials that allow us to concentrate and thus simplify problems (as Browver said: “Mathematics is nothing more, not more which is nothing but the exact part of our thinking "), but you cannot expect that any tool will make your thoughts" right ", because there is no single idea of ​​correctness. IOW, there is no way to formally combine informal and formal: to be informal, to be inside the IO monad is no way out.

So, this does not mean that this syntax reflects my very precise semantics? ", but rather," can I attach my raw semantics to this highly structured syntax? ". Programs are the right material objects, and ideas are cumbersome approximations that can become suitable material objects only by agreement. Thus, we form some basis using conventions, and then we simply trust it, because it is much wiser to trust a small a subset of all your many ideas than all of them.

Answer 4

How do you prove the correctness of mathematics? That is, how do you prove that an integer addition is the right way to count apples, or how do you prove that a real addition is the right way to add weights? There is always an interface between formal / mathematical and informal / real. This requires skill and mathematical / physical taste in order to find a suitable formalism to solve a specific problem. Formal methods do not exclude this.

The value of formal methods is twofold:

• You will not know if your program is correct if you do not know what properties it really satisfies. Before you know if your sorting procedure is correct, you first need to know what it actually does. Any procedure to clarify this issue will be a formal method (even unit testing!), So people who reject “formal methods” actually just limit themselves to a tiny subset of the available methods.

• Even when you know how to find out what the program actually does, people are mistaken in their mathematical reasoning (we are not rational beings, whatever certain ideologies may be); therefore, it is helpful for the machine to test us. This is the same reason we use unit tests. It is nice to check the table and make sure that the program does what we want; but the computer does a check and tells us whether the result helps prevent errors. Providing computers with evidence of our evidence of program behavior is useful for the same reason.

Answer 5

One of the formal methods can do what I don’t think others are affected, is help that connects simple things to more complex ones. You may not know exactly how to specify exactly what the Set data structure should look like, but if you can write a simple version based on sorted lists, you can prove that your fancy version based on balanced search trees is through the toList function. That is, you can use formal methods to transfer your confidence in sorted lists to balanced search trees.

Answer 6

Suppose your function is not the top level, but is used by someone else as part of some module that also has proof of validity. The latter should use the confirmation of the correctness of your function, and if this is bad, the module will not compile. The module itself may still have errors, but it is no longer a problem for you.

Answer 7

A late party, but AFAICT, no one else mentioned another important aspect: in the context of program verification, an error in the specification is not always too terrible, because you can use the code to verify the specification.

IOW, the evidence does not say that the "code is right", but "the code and the specification are mutually agreed." So that the error in the specification does not slow down, it must be one of the following:

• undefined specification.
• error in the specification corresponding to the corresponding error in the code.

As someone else noted: the problem is the same for tests.