AgdaVsCoq

Agda and Coq are both proof assistants based on dependent type theory. Yet they are quite different in several regards. I've tried to list the most important differences here. I'd welcome any feedback and discussion at the bottom of this page.

• Syntax: Although this isn't a deep issue, syntax really matters. Coq's syntax is inspired by ML; Agda's syntax resembles Haskell. Agda has good support for infix/prefix/postfix/mixfix operators and Unicode. You can use Coq's Notation mechanism and Unicode support to achieve similar results. In my experience, however, Agda can be a bit easier on the eye than Coq.
• Interactive development: Agda programs (including proof terms) are usually written interactively using the emacs mode, a bit like repeatedly using the refine tactic in Coq.
• Tactic language: Unlike Coq, Agda doesn't have separate tactic language. You need to write all proofs by hand. There is some automation in the form of Agsy, an automatic proof search tool very similar to Coq's auto tactic.
• Predicativity: Coq is based on the Calculus of Inductive Constructions, an extension of Coquand and Huet's Calculus of Constructions, an impredicative version of Martin-Löf type theory. Agda is a predicative extension of Martin-Löf type theory. Since Coq 8.2, however Set is by default predicative.
• Prop and Set: Coq has a separate Prop type, distinct from Set. Prop is the sort of logical propositions; Set is the sort of data types and computations. The Prop-Set distinction is used by Coq's extraction mechanism which lets you extract an OCaml or Haskell program from a Coq program. Furthermore, Prop is impredicative in Coq. Agda does not have an analogous Prop-Set distinction at the moment.
• Induction-recursion: Agda supports induction-recursion; Coq doesn't. Induction-recursion allows you to define mutually recursive data types and functions. A classic example is a universe closed under Sigma or Pi.
• Pattern matching: In Agda it is quite easy to pattern match on indexed data types (such as Vectors : Nat -> Set). In Coq, this can be a bit more hassle. Coq users may be familiar with the match .. as .. return ... clauses. Agda lets you write pattern matches on such dependent types cleanly, without additional overhead.
• Implicit arguments: In Agda, you must mark which arguments you want to handle implicitly. There is no Set Implicit Arguments command. On the other hand, the syntax for introducing implicit arguments feels a bit more light-weight than in Coq.
• Safety belts: Agda allows you to write non-terminating programs (but warns you if you do). Similarly, you can pass flags to Agda to allow Set : Set or to allow negative recursive occurrences of data types. This allows you to write a program and slowly add more explanation about why it would work.
• Fixed system: Coq is a (reasonably) fixed and theoretically described system – it is an implementation of the Calculus of Inductive Constructions. Agda is more experimental. There is no pen-and-paper description of the underlying theory. As a result, Agda is a bit more open to less established ideas (universe polymorphism, different termination checkers, coinduction, etc.).
• Less is more: Coq is a complex beast. There are lots of cool features and tactics: setoid rewrite, the Program framework, type classes, smart tactics like omega or rewrite, etc. This can make it easy to write quite hard proofs in Coq. In Agda, you need to build such features yourself. While this may seem like a high price to pay, you can sometimes find solutions that fit your problem domain better than Coq's built-in tactics.
• Learning curve: I feel that Agda is a bit easier to learn – there are less features that you need to be familiar with in order to become a proficient Agda user. Although Agda is not without quirks (I can't say I fully understand the algorithm that handles implicit arguments, dot patterns, etc. ), I think that you are less likely to run into incomprehensible errors if you are using Agda than if you are using Coq.

A lot of these claims are based on my limited experience using both systems. As both Coq and Agda are actively developed, I may need to revise this overview. Matthieu Sozeau has been working to improve Coq's treatment of dependent pattern matching and implicit arguments.

I always try to use the best tool for the job. There are plenty of Coq proofs I wouldn't want to write in Agda. But there are quite a few Agda programs, that I wouldn't like to write in Coq.