# HG changeset patch # User Adam Chlipala # Date 1444909320 14400 # Node ID 71b85aaae8682a475bbc05c2f411110ff3018aef # Parent af5de2d0b4edf714c0be321358236b14b45f21cc Fix Epigram URL diff -r af5de2d0b4ed -r 71b85aaae868 src/Intro.v --- a/src/Intro.v Fri Oct 02 12:54:14 2015 -0400 +++ b/src/Intro.v Thu Oct 15 07:42:00 2015 -0400 @@ -117,7 +117,7 @@ (** * Why Not a Different Dependently Typed Language? *) (** -The logic and programming language behind Coq belongs to a type-theory ecosystem with a good number of other thriving members. %\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? +The logic and programming language behind Coq belongs to a type-theory ecosystem with a good number of other thriving members. %\index{Agda}%{{http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php}Agda} and %\index{Epigram}%{{https://code.google.com/p/epigram/}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? I think the answer is simple. None of the competition has well-developed systems for tactic-based theorem proving. Agda and Epigram are designed and marketed more as programming languages than proof assistants. Dependent types are great, because they often help you prove deep theorems without doing anything that feels like proving. Nonetheless, almost any interesting certified programming project will benefit from some activity that deserves to be called proving, and many interesting projects absolutely require semi-automated proving, to protect the sanity of the programmer. Informally, proving is unavoidable when any correctness proof for a program has a structure that does not mirror the structure of the program itself. An example is a compiler correctness proof, which probably proceeds by induction on program execution traces, which have no simple relationship with the structure of the compiler or the structure of the programs it compiles. In building such proofs, a mature system for scripted proof automation is invaluable.