这些程序分别是为什么而设计的，彼此又能为对方提供什么？另外，这两个系统是否一致，而且它们是否基于一些基础数学理论？
我关心的两件事：
我搜索过，我读到的内容似乎非常两极分化，我想从最客观（人性化）的角度了解它们的区别。
【问题讨论】：
Coq 在设计时考虑了定理证明，而 Agda 在设计时考虑了依赖类型编程。
它们在理论上是等价的（尽管它们存在差异，但 Coq 在其公理上稍微保守一些，并且默认情况下更接近 CIC 的数学基础），但在这一点上我几乎同样相信它们。例如，他们都被发现在处理共归纳方面不一致，但对常规归纳部分中的错误非常健壮。
根据我的经验，它们都很容易安装在 Linux 系统上。当 Cabal 工作时，Agda 可能会稍微容易一些，但当它不工作时会更糟糕。 Coq 可以捆绑在一起，或者您可以从源代码构建它，根据我的经验，它还可以，但有时它会变得很痛苦，因为您必须同时关心 OCaml 和camlp5 的版本。
在学习方面，我认为 Coq 可能更容易学习，因为它有一些相当冗长且节奏缓慢的现有书籍（软件基础、Coq'Art 等）和一些高级书籍 (CPDT)。对于 Agda 来说，我的经验有点苛刻，基本上是 Norell 的 PDF 和 wiki ...... 另一方面，Agda 需要较少的学习，因为您主要需要了解依赖类型、语法和标准库。而在 Coq 中，您还必须学习战术，这完全是另一回事！
我的观点是： - 如果你打算用大证明做重大开发，Coq 可能是你安全的选择 - 如果你只是对一些依赖类型的编程感兴趣，Agda 可能是更受欢迎的选择
无论如何，学习其中一个对学习另一个有很大帮助，那么为什么不两者都尝试一下呢？ :)
【讨论】：