# Quote o' the day: proofs and algorithms

Posted on June 12, 2012 by Tommy McGuire
Labels: theory, notation, coq, quote, books, math

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.

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.

Site proudly generated by Hakyll.