Coq 和 Agda 的区别

Posted 2023-02-25

【中文标题】Coq 和 Agda 的区别

【英文标题】：Differences between Coq and Agda

【发布时间】：2014-08-16 11:08:13

【问题描述】：

这些程序分别是为什么而设计的，彼此又能为对方提供什么？另外，这两个系统是否一致，而且它们是否基于一些基础数学理论？

我关心的两件事：

易于安装 简单易学

我搜索过，我读到的内容似乎非常两极分化，我想从最客观（人性化）的角度了解它们的区别。

【问题讨论】：

你看过wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq吗？

刚刚做了，但是有很多我不明白的东西，因为这里假设你至少知道其中之一。

如果那里有你不明白的地方，也许他们很适合在这里问？

【参考方案1】：

Coq 在设计时考虑了定理证明，而 Agda 在设计时考虑了依赖类型编程。

它们在理论上是等价的（尽管它们存在差异，但 Coq 在其公理上稍微保守一些，并且默认情况下更接近 CIC 的数学基础），但在这一点上我几乎同样相信它们。例如，他们都被发现在处理共归纳方面不一致，但对常规归纳部分中的错误非常健壮。

根据我的经验，它们都很容易安装在 Linux 系统上。当 Cabal 工作时，Agda 可能会稍微容易一些，但当它不工作时会更糟糕。 Coq 可以捆绑在一起，或者您可以从源代码构建它，根据我的经验，它还可以，但有时它会变得很痛苦，因为您必须同时关心 OCaml 和camlp5 的版本。

在学习方面，我认为 Coq 可能更容易学习，因为它有一些相当冗长且节奏缓慢的现有书籍（软件基础、Coq'Art 等）和一些高级书籍 (CPDT)。对于 Agda 来说，我的经验有点苛刻，基本上是 Norell 的 PDF 和 wiki ...... 另一方面，Agda 需要较少的学习，因为您主要需要了解依赖类型、语法和标准库。而在 Coq 中，您还必须学习战术，这完全是另一回事！

我的观点是： - 如果你打算用大证明做重大开发，Coq 可能是你安全的选择 - 如果你只是对一些依赖类型的编程感兴趣，Agda 可能是更受欢迎的选择

无论如何，学习其中一个对学习另一个有很大帮助，那么为什么不两者都尝试一下呢？ :)

【讨论】：

另一方面，Agda 的标准库可以被读取以在 FP 中使用依赖类型升级，而它们是 Coq 标准库的重要组成部分，它们太老了，以至于证明风格已被弃用。

现在有一个到 Agda 的端口 ;-) Agda 中的编程语言基础 plfa.github.io