Quote o' the day: proofs and algorithms

This is from the chapter "Basics" of Software Foundations by Benjamin Pierce, et. al.:

"Informal proofs are algorithms; formal proofs are code."

The question of what, exactly, constitutes a "proof" of a mathematical claim has challenged philosophers for millenia. A rough and ready definition, though, could be this: a proof of a mathematical proposition P is a written (or spoken) text that instills in the reader or hearer the certainty that P is true. That is, a proof is an act of communication.

Now, acts of communication may involve different sorts of readers. On one hand, the "reader" can be a program like Coq, in which case the "belief" that is instilled is a simple mechanical check that P can be derived from a certain set of formal logical rules, and the proof is a recipe that guides the program in performing this check. Such recipes are formal proofs.

Alternatively, the reader can be a human being, in which case the proof will be written in English or some other natural language, thus necessarily informal. Here, the criteria for success are less clearly specified. A "good" proof is one that makes the reader believe P. But the same proof may be read by many different readers, some of whom may be convinced by a particular way of phrasing the argument, while others may not be. One reader may be particularly pedantic, inexperienced, or just plain thick-headed; the only way to convince them will be to make the argument in painstaking detail. But another reader, more familiar in the area, may find all this detail so overwhelming that they lose the overall thread. All they want is to be told the main ideas, because it is easier to fill in the details for themselves. Ultimately, there is no universal standard, because there is no single way of writing an informal proof that is guaranteed to convince every conceivable reader. In practice, however, mathematicians have developed a rich set of conventions and idioms for writing about complex mathematical objects that, within a certain community, make communication fairly reliable. The conventions of this stylized form of communication give a fairly clear standard for judging proofs good or bad.

Because we are using Coq in this course, we will be working heavily with formal proofs. But this doesn't mean we can ignore the informal ones! Formal proofs are useful in many ways, but they are not very efficient ways of communicating ideas between human beings.

There's a lot here: the statement in quotes is closely akin to, but subtly different from, the Curry-Howard correspondence, that programs and (formal) proofs are closely related. But there's more, even granted that a formal proof must have more details than an informal proof and that the formal proof may not follow the conventions expected of a traditional informal proof. The proof assistants like Coq that I have looked at produce proofs that are nearly unreadable. For example, this is a proof from Coq (from the Basics chapter just prior to the quote above), of the commutativity of addition:

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n as [| n'].
  Case "n = 0". simpl. rewrite -> plus_0_r. reflexivity.
  Case "n = S n'". simpl. rewrite -> IHn'. rewrite -> plus_n_Sm. reflexivity.
Qed.

It includes the "Case" tactic that helps to document the sub-goals of the inductive proof, which helps immensely. But still.... So, the readability of formal proofs in Coq is significantly worse, to my eyes, than the readability of most programming languages, and as a result translating between a formal proof and an informal, explanatory proof is a difficult skill to learn. It's a good thing Software Foundations has some discussion of it.