这些程序的设计目标是什么？每个程序提供的是另一个程序？此外,两个系统是否一致,而且,它们是否基于一些基础数学理论？
我关心的两件事:
我在搜索,我读到的内容似乎非常两极分化,我想知道他们与最客观(人性)可能的观点的区别.
Pti*_*val 17
Coq的设计考虑了定理,而Agda的设计考虑了依赖类型的编程.
它们在理论方面有些相同(即使它们有差异,Coq在公理中稍微保守一些,并且在默认情况下更接近于CIC的数学基础),但在那一点上我几乎同样相信它们.例如,他们发现它们的共同诱导处理不一致,但对常规诱导部分的错误非常强大.
根据我的经验,它们都很容易安装在Linux系统上.当Cabal工作时,Agda可能会稍微容易一点,但如果没有,则会更加可怕.Coq可以捆绑在一起,或者你可以从源代码构建它,根据我的经验,它是可以的,但有时它会变得很痛苦,因为你必须关心OCaml和camlp5的版本.
在学习方面,我认为Coq可能更容易学习,因为它有一些相当冗长和节奏缓慢的书籍(软件基础,Coq'Art等)和一些高级书籍(CPDT).对于Agda来说,我的体验有点苛刻,基本上是Norell的PDF和wiki ......另一方面,Agda需要较少的学习,因为你大多需要依赖类型,语法和标准库.在Coq你还必须学习其他很多的战术!
我的观点是: - 如果你打算用大证据进行重大开发,Coq可能是你的安全选择 - 如果你只是对一些依赖类型的编程感兴趣,Agda可能是更可爱的选择
学习其中任何一方都会对学习另一方有很大帮助,那么为什么不尝试两者呢？:)