🐇 Coq vs Agda: Which Proof Assistant Should I Learn?

Obligatory Coq advocate checking in 😄. LambdaLynx I think your reasoning for Agda is totally valid for your stated goals, but let me make the case for Coq anyway so you have the full picture.

The thing that converted me was the tactic language. I know term-mode feels elegant in theory, but when you're doing a non-trivial proof, being able to write something like:

...is amazing. You state what you want to prove, Coq shows you the goal state after each tactic, and you just work toward it step by step. It feels more like a conversation with the type-checker than wrestling with it.

Also — and this is the big one for me — mathlib's Coq/Rocq ecosystem is enormous. If you ever want to formalise anything non-trivial, the library support is just on a different level from what Agda currently has.

Worth noting that Agda and Coq share some common ancestry — Thierry Coquand had a hand in both. But they've diverged quite a bit in philosophy. I'd characterise the split roughly as:

• ✓ Agda — dependently-typed functional programming language first, proof assistant second
• ✓ Coq/Rocq — proof assistant first, with a programming sublanguage (Gallina) second

If LambdaLynx's goal is "write correct-by-construction programs," Agda absolutely wins on feel. The hole-driven development workflow is second to none — you put a ? somewhere, Agda tells you the type of the hole and all variables in scope, and you refine from there. It feels like a video game where the type checker is your companion NPC.

You can absolutely write term-mode proofs in Coq too! It's just that for complex things it gets tedious. The tactic language exists precisely to handle cases where the explicit proof term would be dozens of lines of noise. You get the choice between both styles.

And regarding extraction — this is Coq's killer feature that almost never gets mentioned in these comparisons. Coq lets you extract a certified program directly to OCaml, Haskell, or Scheme. The Prop/Set distinction is specifically designed for this: proof-irrelevant Prop terms get erased, and only the computational content in Set remains. Used in production things like the CompCert certified C compiler.

Agda can compile to Haskell too but the extraction story isn't nearly as polished or principled, at least not yet.

Can we talk about termination/productivity checking? Because this is one area where the two tools have genuinely different philosophies and it trips everyone up eventually.

Coq uses a syntactic guardedness check for corecursion — it has to be able to see structurally that recursive calls happen under a constructor (the "guard condition"). It's conservative and sometimes rejects perfectly fine productive definitions.

Agda has sized types as an alternative: you can annotate your coinductive types with a size index, and the termination checker uses these to verify productivity modularly — it works with higher-order functions and polymorphism where the syntactic check would fail. The idea is that sized types track structural descent in the type system itself, making termination checking robust for stronger abstractions.

That said — and this is important — --sized-types and --guardedness are currently mutually inconsistent in Agda when used together under --safe. You have to pick one. It's a known issue and it complicates things a bit.

In practice most Agda code I see uses the default --guardedness for coinduction (coinductive records with the coinductive keyword), which is fine for the common cases. Sized types are the more powerful option but they're also more experimental and carry more proof burden.

To be fair to Coq: Coq is described as a "reasonably fixed and theoretically described system" — it implements the Calculus of Inductive Constructions, which has a clear pen-and-paper description. Agda is more experimental by design, more open to trying new ideas like universe polymorphism and different termination checkers, but that also means some corners are still rough. It's a trade-off between stability and expressiveness.

Not a reason to avoid Agda by any means — just something to be aware of.

Coming in as someone who started with Agda and is now learning Coq for a course: the pattern matching difference is HUGE and I don't think it gets emphasised enough.

In Agda, matching on an indexed type like Vec A n is totally natural — the type indices get refined automatically and everything just works. In Coq you often need to write those match x as y in (SomeType z) return ... dependent pattern match annotations when the return type depends on the scrutinee. It's technically sound but it can feel like the type checker is making you jump through hoops to prove things it should already know.

Writing proof-carrying code with indexed types is generally much more natural in Agda for this reason.

Fair point FunctorFelinae — the convoy pattern is genuinely painful until you internalize it. I'll give Agda that one.

But let me counter on automation. Coq has a sophisticated tactic ecosystem: omega/lia for linear arithmetic, ring and field for algebraic reasoning, auto and eauto for proof search, decide for decidable propositions, and the entire rewrite infrastructure. For a non-trivial proof you're not writing everything by hand — you're orchestrating these automated solvers.

Agda has Agsy, an automatic proof search tool, and the reflection API for writing macros/tactics — but it's much more limited out of the box. You build more things yourself. That's philosophically interesting, but when you're three hours into formalising a number-theory result and ring would have dispatched it in one line... you start to appreciate Coq's batteries.

I want to bring up the Prop/Set distinction in Coq, which MonadicMochi mentioned briefly but deserves more attention. Coq has a separate Prop sort for logical propositions and Set for data types and computations. This is the foundation of the extraction mechanism: anything in Prop is proof-irrelevant and gets erased, while computational content in Set remains in the extracted program.

Agda historically didn't have an analogous Prop/Set distinction, although modern Agda has added a Prop-like universe. But the extraction story in Agda is less mature — if you want to run your verified programs efficiently in a mainstream language, Coq has a clearer path.

The Prop-Set split also enables Coq's impredicative Prop, which is useful for some mathematical formalisations. Agda by contrast is a predicative extension of Martin-Löf type theory throughout.

Good summary LambdaLynx! A few additions:

Re: induction-recursion — it's used in Agda for things like universes (a la Tarski), describing a type theory within type theory, and certain data structure definitions where the type and a function on it must be defined simultaneously. The PLFA book might not exercise it much but if you ever go into meta-theory formalisation it's essential. Coq doesn't have a general IR mechanism.

Also worth adding to your list: Agda's interactive development mode (in Emacs/VS Code via agda-mode) is genuinely one of the best IDE experiences in any dependently typed language. You can case-split, refine goals, auto-search, and normalize terms all without leaving your editor. It's not just useful, it's genuinely fun in a way that's hard to describe until you've done it.

Coq's Proof General / CoqIDE / VSCoq is also good! But I personally find Agda's interaction model more tightly integrated with the proof/program itself.

First post in this subforum — been reading as a lurker for ages. Hope it's okay to chime in!

I'm a newer learner and went with Agda first. The thing that surprised me was how much the Unicode matters psychologically. Like, writing ∀ (n : ℕ) → n + 0 ≡ n instead of forall n : nat, n + 0 = n doesn't change the math at all, but it makes me feel like I'm writing actual mathematics rather than encoding it in a programming language. That feeling matters for motivation.

The mixfix operators are also super powerful — you can define things like:

...and then use it literally as if b then x else y. Agda name parts separated by underscores become operator positions. That level of notation control is really powerful for writing readable specifications.

RecursiveTabbyCat welcome!! Great first post.

The Unicode thing is genuinely a taste split in the community. Some people love it (including apparently most of us in this thread 😄). Others find it annoying because:

• You have to learn all the input key sequences (though agda-mode makes this manageable)
• It can be hard to diff/grep/search code with non-ASCII symbols
• Some symbols look identical to different Unicode characters (→ vs -> vs some similar-looking arrow)

Coq recently got much better Unicode support too (you can use → and ∀ in Coq), so this gap has narrowed. But Agda's support is still more deeply embedded in the language identity — the standard library basically requires Unicode fluency.

I want to push back gently on the "Coq proofs feel separate from programs" criticism. Modern Coq with Program, type classes, and Equations plugin does a lot to blur that line. You can write very programming-oriented Coq these days.

Mod hat off, personal opinion hat on: I've used both seriously for research.

For LambdaLynx's specific stated goal — writing correct-by-construction programs, coming from Haskell, wanting code-and-proof to feel unified — Agda is the better choice. This is not a close call. The hole-driven, term-mode workflow is exactly what you want for that style of programming, and the clean dependent pattern matching will save you enormous pain.

For formalising mathematics — especially if you want to build on existing results, use ring/lia/omega, or eventually want to work with anything near mathlib — Coq/Lean is the way to go. Coq's ecosystem maturity and proof automation story is just miles ahead for this use case.

The good news is that if you learn one seriously, the concepts transfer pretty well. The dependent type theory fundamentals are the same — Martin-Löf type theory with inductive families, the Curry-Howard correspondence, universe hierarchies. You'll be surprised how much translates once you know one well.

Mod note: keeping this thread open, everyone's been lovely. No rule violations. 🌸 Please continue!

Something nobody has mentioned: learning curve. In my experience Agda is actually somewhat easier to get started with — there are fewer features you need to be familiar with to become productive. You don't need to learn a tactic language on top of a type theory; there's just the type theory.

Coq is a larger, more complex beast. Type classes, setoid rewriting, the Program framework, tactic combinators, Ltac, Ltac2... there's a lot of surface area to cover before you feel truly proficient. The payoff is worth it if math formalisation is your goal, but it's a bigger investment upfront.

For someone coming from Haskell who already thinks in terms of types and functions, Agda slots in very naturally. It's basically "Haskell with dependent types and totality" as a first approximation.

Quick note on tooling and editor support since KleisliKitten mentioned it — both have good options now:

Agda: agda-mode for Emacs (the canonical, most complete), agda-mode-vscode (surprisingly good now), vim via cornelis. The Emacs mode is particularly tightly integrated — it was basically designed around Emacs interaction.

Coq: Proof General (Emacs, battle-tested), CoqIDE (standalone), VSCoq (VS Code, now officially maintained). Rocq rebranding is ongoing so some docs refer to "Coq" and some to "Rocq".

Also worth mentioning that Agda has cubical mode (--cubical) which gives you univalence and higher inductive types for free. That's a really big deal if you want to do HoTT. Coq has the HoTT library but cubical Agda is more natively supported. But that's probably more advanced than what LambdaLynx needs right now!

I'll concede the pattern matching and learning curve points. Those are real. Let me make one final case for Coq from a different angle: community resources and hiring.

If you ever want to work somewhere that uses formal verification (Amazon AWS, some automotive/aerospace contractors, certain research labs), Coq experience is far more recognised. CompCert, seL4 (well, that's Isabelle actually), the verified concurrent garbage collector work, the VST project... Coq has a track record in industry that Agda simply doesn't yet have to the same degree.

Software Foundations is also one of the best introductory programming languages textbooks written in the last decade, period. The Coq ecosystem around learning material is just incredibly mature at this point.

...That said, I'm starting to think LambdaLynx should just go with Agda 😂. You've clearly already made up your mind and everything being said here confirms your intuition. Sometimes the right answer is just "do the thing that sounds fun to you."

Congrats on the decision! One practical tip before you dive in: set up your editor properly first before writing a single line of Agda. This is not optional advice. Agda without an interactive mode is like trying to play Minecraft without a mouse. The interaction model IS the language experience.

Install agda-mode for Emacs (preferred) or agda-mode-vscode for VS Code. Learn these keybindings at minimum:

Once these are muscle memory you'll never want to write code without a type-checker companion NPC again 🎮

Happy to have helped, even if I ultimately advocated myself into a loss 😂. The Coq case is real and remains my personal preference — but CubicalCatgirl and FunctorFelinae are right that for your goals, Agda fits better.

Maybe we can do a follow-up thread: "I learned Agda — now what do I do with it?" I expect great answers involving things like MLTT in Agda, normalization by evaluation, and the inevitable implementing a type checker in the thing you learned to type-check pipeline that we all eventually fall into.

Good luck LambdaLynx! And everyone else reading this thread who's on the fence: the real answer is that both are worth your time. Start with whichever matches your goals and don't let anyone (including me) talk you out of it.

— MonadicMochi, reluctant Agda supporter, unconditional Coq enjoyer 🍡