Coq是一个证明助手，而Agda/Idris则是编程语言（尽管它们也可以被称为证明助手）。
我正在探索这些语言，想知道Agda/Idris是否足以做到Coq所能做的一切。
那么，有没有一些[证明/管理代码/IDE（Emacs）功能/其他事情]，是Coq可以做而Agda/Idris做不到的？
Coq与Agda/Idris相比有什么优势？
9
- ice1000
4
3Coq作为一种编程语言，类似于Agda（其主要区别在于模式匹配和“宇宙”）。我对Idris并不是专家，但我认为Coq和Agda比Idris具有更强的“逻辑能力”。其中，Coq与这些语言的不同之处在于其支持策略、符号、提取和广泛的库支持。这些在实践中都是非常重要的因素。此外，Coq的性能虽然不是最好的，但在实际意义上是稳健的。而且，如果不考虑模块，内核相对较小。 - ejgallego
2@ejgallego 关于归纳递归怎么样？或者大小类型？或者基于共模式的对共归纳数据的处理？或者 Streicher 的 K？或者隐式绑定器？或者规范结构？这些系统确实非常相似，但它们之间也有着非常重要的特性/设计选择来区分它们。 - gallais
当然，@gallais，我之所以写了评论而不是答案，是因为写好答案并不容易。 - ejgallego
2好的。至于Idris，这里有一个相关的SO问题：https://dev59.com/Hmox5IYBdhLWcg3wCQEq - gallais
1个回答
7
Coq已经存在了一段时间，并且有着强大的社区和许多库和开发。它还具有策略语言和其他一些扩展，使其非常适合于更大的项目。
就Coq核心语言而言，它通常比Agda提供的要少。例如，很难通过模式匹配定义函数（尽管有一个扩展可以帮助）它不具有归纳-归纳类型或混合归纳和余归纳。大多数Coq开发不使用依赖类型（因为它们在Coq中很难使用），而是使用简单（或多态类型）程序与上面的谓词的组合。
- Thorsten Altenkirch
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接