Differences between Coq and Agda

Question

What are each of these programs designed for and what does each offer other the other? Also, are both systems consistent, and moreover, are they based on some foundational mathematical theory?

Two things I care about:

1. Easy to install
2. Easy to learn

I've search and what I've read seems very polarized, I would like to know their differences from the most objective (humanly) possible perspective.

Answer 1

Coq has been designed with theorem proving in mind, whereas Agda has been designed with dependently-typed programming in mind.

They are somewhat equivalent on the theoretical side (even though they have differences, Coq being slightly more conservative in its axioms and sticking closer to the mathematical foundation of CIC by default), but I would trust them almost equally at that point. For instance, they have both been found to be inconsistent in their treatment of coinduction, but are pretty robust to bugs in the regular inductive part.

In my experience they are both easy to install on a Linux system. Agda might be slightly easier when Cabal works, but more terrible when it doesn't. Coq can come bundled or you can build it from source, in my experience it's been ok, but sometimes it gets painful because you have to care about versions of both OCaml and camlp5.

In terms of learning, I think Coq might be easier to learn because it has some existing books that are fairly lengthy and slow-paced (Software Foundations, Coq'Art, etc.) and some advanced books (CPDT). For Agda it's been a bit harsher in my experience, basically Norell's PDF and the wiki... On the other hand, Agda requires less learning because you mostly have to grok dependent types, the syntax, and the standard library. Whereas in Coq you also have to learn about tactics which is a whole other lot!

My point of view would be: - if you intend to do major developement with big proofs, Coq is probably your safe choice - if you are just interested in programming with some dependent types, Agda is probably the more likeable choice

Learning either will help a lot in learning the other anyway, so why not try a bit of both? :)