What to prove and how to prove it 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:


What exactly we are proving.
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).
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).
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
   | [] =&gt; 0
   | x::xs =&gt; x + sum xs


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

 Inductive Is_Sum : Nat -&gt; List Nat -&gt; Prop :=
    | IS_Empty : Is_Sum 0 []
    | IS_Cons : Is_Sum s xs -&gt; 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 -&gt; x &lt;= 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.