@@ -51,7 +51,7 @@ There are a good number of (though definitely not %``%#"#many#"#%''%) tools that
...
@@ -51,7 +51,7 @@ There are a good number of (though definitely not %``%#"#many#"#%''%) tools that
</table>
</table>
#
#
Isabelle/HOL,implementedwiththe%``%#"#proof assistant development framework#"#%''%Isabelle%~\cite{Isabelle}%,isthemostpopularproofassistantfortheHOLlogic.TheotherimplementationsofHOLcanbeconsideredequivalentforpurposesofthediscussionhere.
Isabelle/HOL,implementedwiththe"proof assistant development framework"Isabelle%~\cite{Isabelle}%,isthemostpopularproofassistantfortheHOLlogic.TheotherimplementationsofHOLcanbeconsideredequivalentforpurposesofthediscussionhere.
*)
*)
...
@@ -88,9 +88,9 @@ Dependent types are not just useful because they help you express correctness pr
...
@@ -88,9 +88,9 @@ Dependent types are not just useful because they help you express correctness pr
%\index{Isabelle/HOL}%Isabelle/HOLandCoqbothsupportcodingnewproofmanipulationsinMLinwaysthatcannotleadtotheacceptanceofinvalidproofs.Additionally,Coqincludesadomain-specificlanguageforcodingdecisionproceduresinnormalCoqsourcecode,withnoneedtobreakoutintoML.Thislanguageiscalled%\index{Ltac}%Ltac,andIthinkofitastheunsungherooftheproofassistantworld.NotonlydoesLtacpreventyoufrommakingfatalmistakes,italsoincludesanumberofnovelprogrammingconstructswhichcombinetomakea%``%#"#proof by decision procedure#"#%''%styleverypleasant.Wewillmeetthesefeaturesinthechapterstocome.
%\index{Isabelle/HOL}%Isabelle/HOLandCoqbothsupportcodingnewproofmanipulationsinMLinwaysthatcannotleadtotheacceptanceofinvalidproofs.Additionally,Coqincludesadomain-specificlanguageforcodingdecisionproceduresinnormalCoqsourcecode,withnoneedtobreakoutintoML.Thislanguageiscalled%\index{Ltac}%Ltac,andIthinkofitastheunsungherooftheproofassistantworld.NotonlydoesLtacpreventyoufrommakingfatalmistakes,italsoincludesanumberofnovelprogrammingconstructswhichcombinetomakea"proof by decision procedure"styleverypleasant.Wewillmeetthesefeaturesinthechapterstocome.
@@ -117,22 +117,22 @@ The critical ingredient for this technique, many of whose instances are referred
...
@@ -117,22 +117,22 @@ The critical ingredient for this technique, many of whose instances are referred
(***WhyNotaDifferentDependentlyTypedLanguage?*)
(***WhyNotaDifferentDependentlyTypedLanguage?*)
(**
(**
ThelogicandprogramminglanguagebehindCoqbelongstoatype-theoryecosystemwithagoodnumberofotherthrivingmembers.%\index{Agda}Agda\footnote{\url{http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php}}%#<a href="http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php">Agda</a># and %\index{Epigram}Epigram\footnote{\url{http://www.e-pig.org/}}%#<a href="http://www.e-pig.org/">Epigram</a># are the most developed tools among the alternatives to Coq, and there are others that are earlier in their lifecycles. All of the languages in this family feel sort of like different historical offshoots of Latin. The hardest conceptual epiphanies are, for the most part, portable among all the languages. Given this, why choose Coq for certified programming?
ThelogicandprogramminglanguagebehindCoqbelongstoatype-theoryecosystemwithagoodnumberofotherthrivingmembers.%\index{Agda}%{{http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php}Agda} and %\index{Epigram}%{{http://www.e-pig.org/}Epigram} are the most developed tools among the alternatives to Coq, and there are others that are earlier in their lifecycles. All of the languages in this family feel sort of like different historical offshoots of Latin. The hardest conceptual epiphanies are, for the most part, portable among all the languages. Given this, why choose Coq for certified programming?
Incomparisonswithitscompetitors,Coqisoftenderidedforpromotingunreadableproofs.Itisveryeasytowriteproofscriptsthatmanipulateproofgoalsimperatively,withnostructuretoaidreaders.Suchdevelopmentsarenightmarestomaintain,andtheycertainlydonotmanagetoconvey%``%#"#why the theorem is true#"#%''%toanyonebuttheoriginalauthor.Oneadditional(andnotinsignificant)purposeofthisbookistoshowwhyitisunfairandunproductivetodismissCoqbasedontheexistenceofsuchdevelopments.
Incomparisonswithitscompetitors,Coqisoftenderidedforpromotingunreadableproofs.Itisveryeasytowriteproofscriptsthatmanipulateproofgoalsimperatively,withnostructuretoaidreaders.Suchdevelopmentsarenightmarestomaintain,andtheycertainlydonotmanagetoconvey"why the theorem is true"toanyonebuttheoriginalauthor.Oneadditional(andnotinsignificant)purposeofthisbookistoshowwhyitisunfairandunproductivetodismissCoqbasedontheexistenceofsuchdevelopments.
%\index{graphicalinterfacestoCoq}%IbelievethatagoodgraphicalinterfacetoCoqiscrucialforusingitproductively.Iusethe%\index{ProofGeneral}ProofGeneral\footnote{\url{http://proofgeneral.inf.ed.ac.uk/}}%#<a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a># mode for Emacs, which supports a number of other proof assistants besides Coq. There is also the standalone %\index{CoqIDE}%CoqIDE program developed by the Coq team. I like being able to combine certified programming and proving with other kinds of work inside the same full-featured editor, and CoqIDE has had a good number of crashes and other annoying bugs in recent history, though I hear that it is improving. In the initial part of this book, I will reference Proof General procedures explicitly, in introducing how to use Coq, but most of the book will be interface-agnostic, so feel free to use CoqIDE if you prefer it. The one issue with CoqIDE, regarding running through the book source, is that I will sometimes begin a proof attempt but cancel it with the Coq [Abort] or #<span class="inlinecode"><span class="id" type="keyword">#%\coqdockw{%Restart%}%#</span></span># commands, which CoqIDE does not support. It would be bad form to leave such commands lying around in a real, finished development, but I find these commands helpful in writing single source files that trace a user's thought process in designing a proof.
%\index{graphicalinterfacestoCoq}%IbelievethatagoodgraphicalinterfacetoCoqiscrucialforusingitproductively.Iusethe%\index{ProofGeneral}%{{http://proofgeneral.inf.ed.ac.uk/}Proof General} mode for Emacs, which supports a number of other proof assistants besides Coq. There is also the standalone %\index{CoqIDE}%CoqIDE program developed by the Coq team. I like being able to combine certified programming and proving with other kinds of work inside the same full-featured editor, and CoqIDE has had a good number of crashes and other annoying bugs in recent history, though I hear that it is improving. In the initial part of this book, I will reference Proof General procedures explicitly, in introducing how to use Coq, but most of the book will be interface-agnostic, so feel free to use CoqIDE if you prefer it. The one issue with CoqIDE, regarding running through the book source, is that I will sometimes begin a proof attempt but cancel it with the Coq [Abort] or #<span class="inlinecode"><span class="id" type="keyword">#%\coqdockw{%Restart%}%#</span></span># commands, which CoqIDE does not support. It would be bad form to leave such commands lying around in a real, finished development, but I find these commands helpful in writing single source files that trace a user's thought process in designing a proof.
*)
*)
(****ReadingThisBook*)
(****ReadingThisBook*)
...
@@ -181,7 +181,7 @@ Previous versions of the book included some suggested exercises at the ends of c
...
@@ -181,7 +181,7 @@ Previous versions of the book included some suggested exercises at the ends of c