这些程序各自设计用于什么，并且它们各自提供了什么？此外，两个系统是否一致，并且它们是否基于某种基础数学理论？
我关心的两件事：
- 易于安装
- 易于学习
我已经进行了搜索，所读到的似乎非常极端，我想从最客观（人类）的角度了解它们之间的区别。
1个回答
35
Coq是为定理证明而设计的，而Agda则是为依赖类型编程而设计的。
从理论上讲，它们有点等效（尽管它们存在差异，Coq在其公理方面略微保守，并默认更接近CIC的数学基础），但在这一点上我几乎同等信任它们。例如，它们都被发现在处理共归性时不一致，但在常规归纳部分中非常强大，可以缓解错误。
根据我的经验，它们都很容易在Linux系统上安装。当Cabal正常工作时，Agda可能会稍微容易些，但当Cabal不正常时则更糟糕。Coq可以捆绑或从源代码构建，在我的经验中，这还可以，但有时会变得很痛苦，因为您必须关心OCaml和camlp5的版本。
在学习方面，我认为Coq可能更容易学习，因为它有一些现有的书籍相当冗长、节奏缓慢（如Software Foundations、Coq'Art等）和一些高级书籍（CPDT）。对于Agda来说，根据我的经验，情况有点艰难，基本上是Norell的PDF和维基......另一方面，Agda需要更少的学习，因为您主要必须掌握依赖类型、语法和标准库。而在Coq中，您还必须学习策略，这是另一种重要的技能！
我的观点是： - 如果你打算进行大规模的开发并有大量证明工作，Coq可能是你安全的选择 - 如果你只是对编程中的某些依赖类型感兴趣，那么Agda可能更受欢迎
无论哪种方式，学习任何一种都会对学习另一种有很大帮助，所以为什么不尝试一下两种呢？ :)
- Ptival
2
9另一方面，Agda的标准库可以被阅读为使用依赖类型进行函数式编程的提升，而Coq的标准库中有很大一部分已经过时，证明风格已经不再推荐使用。 - gallais
9现在已经有 Agda 的端口了；-）
Agda中的编程语言基础 https://plfa-zh.github.io/ - Musa Al-hassy
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接