# 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.

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.