Define 'certified program'

src/Intro.v

@@ -22,6 +22,10 @@ Around the beginning of the 21st century, the pace of progress in practical appl
 
 Many other recent projects have attracted attention by proving important theorems using computer proof assistant software.  For instance, the L4.verified project%~\cite{seL4}% has given a mechanized proof of correctness for a realistic microkernel, using the Isabelle/HOL proof assistant%~\cite{Isabelle/HOL}\index{Isabelle/HOL}%.  The amount of ongoing work in the area is so large that I cannot hope to list all the recent successes, so from this point I will assume that the reader is convinced both that we ought to want machine-checked proofs and that they seem to be feasible to produce.  (To readers not yet convinced, I suggest a Web search for %``%#"#machine-checked proof#"#%''%!)
 
+The idea of %\index{certified program}\emph{%#<i>#certified program#</i>#%}% features prominently in this book's title.  Here the word %``%#"#certified#"#%''% does %\emph{%#<i>#not#</i>#%}% refer to governmental rules for how the reliability of engineered systems may be demonstrated to sufficiently high standards.  Rather, this concept of certification, a standard one in the programming languages and formal methods communities, has to do with the idea of a %\emph{%#<i>#certificate#</i>#%}%, or formal mathematical artifact proving that a program meets its specification.  Government certification procedures rarely provide strong mathematical guarantees, while certified programming provides guarantees about as strong as anything we could hope for.  We trust the definition of a foundational mathematical logic, we trust an implementation of the logic, and we trust that we have encoded our informal intent properly in formal specifications, but little else is left open as an opportunity to certify incorrect software.  For programs like compilers that run in batch mode, the notion of a %\index{certifying program}\emph{%#<i>#certifying#</i>#%}% program is also common, where each run of the program outputs both an answer and a proof that it is correct.  Certified software can be considered to subsume certifying software, and this book focuses on the certified case, while also introducing principles and techniques of general interest for stating and proving theorems in Coq.
+
+%\medskip%
+
 There are a good number of (though definitely not %``%#"#many#"#%''%) tools that are in wide use today for building machine-checked mathematical proofs and machine-certified programs.  The following is my attempt at an exhaustive list of interactive %``%#"#proof assistants#"#%''% satisfying a few criteria.  First, the authors of each tool must intend for it to be put to use for software-related applications.  Second, there must have been enough engineering effort put into the tool that someone not doing research on the tool itself would feel his time was well spent using it.  A third criterion is more of an empirical validation of the second: the tool must have a significant user community outside of its own development team.
 
 %