Wofür sind diese Programme konzipiert und was bietet jedes andere an? Sind beide Systeme konsistent, und basieren sie außerdem auf einer grundlegenden mathematischen Theorie?Unterschiede zwischen Coq und Agda
Zwei Dinge, die ich kümmern uns um:
Ich suche habe zu lernen, und was ich scheint sehr polarisiert lesen, ich würde gerne wissen, ihre Unterschiede von der objektivsten (menschlich) möglichen Perspektive.
Coq wurde im Hinblick auf den Theorembeweis entwickelt, während Agda im Hinblick auf die abhängige Programmierung entwickelt wurde.
Sie sind auf der theoretischen Seite etwas äquivalent (obwohl sie Unterschiede haben, Coq ist etwas konservativer in seinen Axiomen und klebt näher an der mathematischen Grundlage von CIC), aber ich würde ihnen an diesem Punkt fast gleich vertrauen . Zum Beispiel wurde festgestellt, dass beide in ihrer Behandlung der Coinduktion inkonsistent sind, aber sie sind gegenüber Fehlern im regulären induktiven Teil ziemlich robust.
Nach meiner Erfahrung sind sie beide einfach auf einem Linux-System zu installieren. Agda könnte etwas leichter sein, wenn Cabal funktioniert, aber schrecklicher, wenn es nicht klappt. Coq kann gebündelt geliefert werden oder Sie können es aus der Quelle erstellen, nach meiner Erfahrung war es in Ordnung, aber manchmal wird es schmerzhaft, weil Sie sich um Versionen von OCaml und Camlp5 kümmern müssen.
In Bezug auf das Lernen, denke ich, Coq könnte leichter zu lernen, weil es einige vorhandene Bücher, die ziemlich lang und langsam (Software Foundations, Coq'Art, etc.) und einige erweiterte Bücher (CPDT) hat. Für Agda war es ein bisschen härter in meiner Erfahrung, im Grunde Norells PDF und das Wiki ... Auf der anderen Seite erfordert Agda weniger Lernen, weil Sie meistens abhängige Typen, die Syntax und die Standardbibliothek finden müssen. Während man in Coq auch etwas über Taktiken lernen muss, ist das eine ganz andere Sache!
Meine Sicht wäre: - wenn Sie wichtige Entwicklung mit großen Beweisen zu tun beabsichtigen, Coq ist wahrscheinlich die sichere Wahl - wenn Sie nur daran interessiert in der Programmierung mit einigen abhängigen Typen sind, Agda ist wahrscheinlich die sympathische Wahl
Lernen entweder wird viel helfen, die anderen sowieso zu lernen, also warum nicht ein bisschen von beiden versuchen? :)
Auf der anderen Seite kann Agdas Standard-Bibliothek gelesen werden, um in FP mit abhängigen Typen zu leben, während sie große Teile der Coq-Standard-Bibliothek sind, die so alt sind, dass der Beweis-Stil veraltet ist. – gallais
Haben Sie sich http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq angeschaut? – user3237465
Habe ich gerade, aber es gibt viele Dinge, die ich nicht verstehe, da dies voraussetzt, dass du zumindest einen von ihnen kennst. –
Wenn es Dinge gibt, die du dort nicht verstehst, wären sie vielleicht gut geeignet, um hier zu fragen? – didierc