Coq was designed based on the theorem, while Agda was designed based on type-specific programming.
They are somewhat equivalent to the theoretical side (although they have differences, Coq is somewhat more conservative in its axioms and approaches the mathematical basis of CIC by default), but I would trust them almost equally at this point. For example, they were recognized as inconsistent in their treatment of coin formation, but they were quite resistant to errors in the usual inductive part.
In my experience, they are easy to install on a Linux system. Agda may be a little lighter when Cabal is running, but more scary when it is not. Coq can be bundled or you can build it from the source, in my experience this was fine, but sometimes it gets painful because you need to take care of the OCaml and camlp5 versions.
Regarding training, I think Coq might be easier to learn because it has several existing books that are quite long and slow (Software Foundations, Coq'Art, etc.) and some advanced books (CPDT). For Agda, it was a little harsh in my experience, mostly Norell PDF and wiki ... On the other hand, Agda requires less training because you basically have to look for dependent types, syntax, and a standard library. While at Coq, you also need to learn about tactics that are a whole host!
My point: - if you intend to do major development with great evidence, Coq is probably your safe choice - if you are just interested in programming with some dependent types, Agda is probably a more pleasant choice
Learning will either help others learn a lot anyway, so why not try a little? :)
Ptival
source share