这些程序分别是为什么设计的，彼此又能提供什么？而且，两个系统是否一致，而且它们是否基于某种基础数学理论？
我关心的两件事:
我已经搜索过，并且阅读的内容似乎是两极分化的，我想从最客观(人类)的 Angular 来了解它们之间的差异。
最佳答案
Coq的设计考虑了定理，而Agda的设计考虑了依赖类型的编程。
它们在理论上是等效的(即使它们之间存在差异，Coq的公理稍微保守一些，并且默认情况下更接近CIC的数学基础)，但是在那一点上我几乎可以信任它们。例如，发现它们在共感处理中都不一致，但是对常规归纳部分中的错误相当健壮。
以我的经验，它们都很容易安装在Linux系统上。当Cabal工作时，Agda可能会稍微容易一些，但是当Cabal工作时，Agda会更糟糕。 Coq可以 bundle 在一起，也可以从源代码构建，我认为还可以，但是有时会很痛苦，因为您必须关心OCaml和camlp5的版本。
在学习方面，我认为Coq可能更容易学习，因为它有一些既长又慢的现有书籍(软件基础，Coq'Art等)和一些高级书籍(CPDT)。对于阿格达(Agda)而言，我的经验更加苛刻，基本上是诺雷(Norell)的PDF和Wiki ...
另一方面，Agda需要较少的学习，因为您大多不得不依赖于依赖类型，语法和标准库。而在Coq中，您还必须学习有关战术的知识!
我的观点是:
-如果您打算使用大量证据进行重大开发，那么Coq可能是您的安全选择
-如果您仅对使用某些依赖类型进行编程感兴趣，那么Agda可能是更受欢迎的选择
无论如何，学习任何一个都会对学习另一个有很大帮助，那么为什么不尝试两者呢？ :)
关于coq - Coq和Agda之间的差异，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/24416252/