@@ -117,7 +117,7 @@ The critical ingredient for this technique, many of whose instances are referred
...
@@ -117,7 +117,7 @@ The critical ingredient for this technique, many of whose instances are referred
(***WhyNotaDifferentDependentlyTypedLanguage?*)
(***WhyNotaDifferentDependentlyTypedLanguage?*)
(**
(**
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?
ThelogicandprogramminglanguagebehindCoqbelongstoatype-theoryecosystemwithagoodnumberofotherthrivingmembers.%\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?