What to prove and how to prove it

Question

In learning about proof theory, I am interested to know how to go about "proving properties of a program". I don't exactly see yet what needs to be proven, nor how to prove it, which leads to this brief discussion followed by some questions.

In some languages (such as TLA+), the program is the specification (I think). If not TLA+, maybe you can do that in Coq, but I've heard of it. So that means roughly that what you write is automatically proven. But if that is the case, how do you prove that it's proven. It seems that at some point you have to actually test both the code and the proofs and see that it does what the specification says. Some basic TDD.

In reviewing the Curry-Howard correspondence, programs are proofs, or at least lambda/functional/logic style programs. Not really sure what this means in practice. If simply writing a new function that implements a specification means we have a proof, or what.

So the questions are:

1. What exactly we are proving.
2. How do we prove that the system meets the specification (if the language is or is not the actual specification). If I write code that says "I will always handle this HTTP request error by tracing its output to the console", and that is "specified" in the specification, then how does it get proven. Not sure what I do to say "guaranteed, this behavior will happen". In my head the only way this can be proven is by actually doing tests on the code (i.e. model testing or just brute force simulation testing like you would see in TDD).
3. When writing tests (as in TDD) comes into play when creating these proofs. Wondering if proofs need tests, sorta thing, or at what point you are done with your proof being proven.

So it seems that what we want to prove is that the system behaves as expected. And given we have defined how we want the system to work, the question is how to prove it matches the specification, at a high level. How much do we prove, how do we know the proofs actually prove what we want and the behavior will be what we want (and proven).

Answer 1

I think you raise an important point, which is that in a high level language, specifications can be hard to distinguish from implementations. For example, in Coq, the specification of "The sum of the elements of a list of naturals" is probably going to look something like:

Fixpoint sum (l : List Nat) : Nat :=
  match l with
   | [] => 0
   | x::xs => x + sum xs

It's hard to imagine what the specification of this would be, other than some predicate like

 Inductive Is_Sum : Nat -> List Nat -> Prop :=
    | IS_Empty : Is_Sum 0 []
    | IS_Cons : Is_Sum s xs -> Is_Sum (x + s) (x::xs)

which really just seems like a re-formulation in terms of logic programming. Indeed it is very easy to show forall l : List Nat, Is_Sum (sum l) l.

At this point, it is indeed possible to test the definition of sum and make sure it lines up with our intuition, e.g. check sum [1,2,3] = 6. However, there is an important other step we can check in terms of "specification checking", that of proving derived properties. For sum, we could prove

Proposition sum_append : forall l1 l2, sum (l1 ++ l2) = sum l1 + sum l2

or

Proposition sum_leq : forall l x, In x l -> x <= sum l

These propositions establish the consistency of our definition against some of our intuitions, and avoid certain silly mistakes, e.g. if we had returned $1$ instead of $0$ for the empty list.

Indeed, often for our purposes the properties we actually are interested are the derived properties! Defining the full specification is only a means to an end, like strengthening the induction hypothesis.

Finally, it's probably useful to note that in real life, our specifications are often much simpler than our implementations! Indeed, if our implementations are doing nothing clever, then why do we care so much about proving them correct? (well, actually even the simplest of programs might benefit from proofs.)

One rather simple example is merge sort which while pretty straight forward, is certainly complex enough to warrant a proof of correctness, and at any rate is very different looking than its specification.

Answer 2

It's not correct to say that in TLA+, the program is the specification. I don't know of any system where that is true.

Rather, TLA+ is a way of writing a formal model of a system. You could think of that as a program. Then, we want to verify some property of that program. The property must be specified separately. For instance, the model might describe how a traffic light changes states (e.g., from green in one direction, to yellow in that direction, to red in that direction and green in another, etc.); the property might describe something we want to be true about that model (e.g., that it never shows green in two opposing directions at the same time). So, no, the program is not the specification; they are two separate things.

I think once you clear up that misconception, the question evaporates. The property describes what we want to prove; the program is the thing we want to prove it about.

---

Regarding your comment: executable specifications are executable and as such can be considered as a program, but that doesn't mean the program is the specification. I suggest doing some more reading. For instance, try reading about refinement and simulation relations (Wikipedia won't be enough; try to find a textbook on model checking and formal verification). Here we might have two programs; one is the implementation we want to prove something about, the second is the specification, and we show that the first refines the second. That lets us prove something useful about the first.