title: Definition of a certified program
body: <p>I see a couple of different research groups, and at least one book, that talk about using Coq for designing certified programs.  Is there are consensus on what the definition of <em>certified program</em> is?  From what I can tell, all it really means is that the program was proved total and type correct.  Now, the program's type may be something really exotic such as a list with a proof that it's nonempty, sorted, with all elements >= 5, etc.  However, ultimately, is a certified program just one that Coq shows is total and type safe, where all the interesting questions boil down to what was included in the final type?</p>
  
  <hr>
  
  <h1>Edit 1</h1>
  
  <p>Based on wjedynak's answer, I had a look at Xavier Leroy's paper "Formal Verification of a Realistic Compiler", which is linked in the answers below.  I think this contains some good information, but I think the more informative information in this sequence of research can be found in the paper <a href="http://pauillac.inria.fr/~xleroy/publi/Clight.pdf" rel="noreferrer">Mechanized Semantics for the Clight Subset of the C Language</a> by Sandrine Blazy and Xavier Leroy.  This is the language that the "Formal Verification" paper adds optimizations to.  In it, Blazy and Leroy present the syntax and semantics of the Clight language and then discuss the validation of these semantics in section 5.  In section 5, there's a list of different strategies used for validating the compiler, which in some sense provides an overview of different strategies for creating a <em>certified program</em>.  These are:</p>
  
  <ol>
  <li>Manual reviews</li>
  <li>Proving properties of the semantics</li>
  <li>Verified translations</li>
  <li>Testing executable semantics</li>
  <li>Equivalence with alternate semantics</li>
  </ol>
  
  <p>In any case, there are probably points that could be added and I'd certainly like to hear about more.</p>
  
  <p>Going back to my original question of what the definition is of a certified program, it's still a little unclear to me.  Wjedynak sort of provides an answer, but really the work by Leroy involved creating a compiler in Coq and then, in some sense, certifying it.  In theory, it makes it possible to now prove things about the C programs since we can now go C->Coq->proof.  In that sense, it seems like there's this work flow where we could</p>
  
  <ol>
  <li>Write a program in X language</li>
  <li>Form of a model of the program from step 1 in Coq or some other proof assistant tool.  This could involve creating a model of the programming language in Coq or it could involve creating a model of the program directly (i.e. rewriting the program itself in Coq).</li>
  <li>Prove some property about the model.  Maybe it's a proof about the values.  Maybe it's the proof of the equivalence of statements (stuff like 3=1+2 or f(x,y)=f(y,x), whatever.)</li>
  <li>Then, based on these proofs, call the original program certified.</li>
  </ol>
  
  <p>Alternatively, we could create a specification of a program in a proof assistant tool and then prove properties about the specification, but not the program itself.</p>
  
  <p>In any case, I'm still interested in hearing alternative definitions if anyone has them.</p>