# Agda

19 Hacker News commenters recommended Agda and 5 criticized it, November 2025 to November 2026. It was recommended in 9 of 13 months. It meets the Hacker Approved badge rule.

**Verdict:** Dependently typed proof assistant people prefer for interactive proof checking and math exploration; critics say it is impractical for building ordinary software and has little AI training data.

## Why people recommend it

- Preferred for interactive proof checking (3 comments): "uses the Agda proof assistant in exactly this sense, as a kind of interactive blackboard for taking notes" ([source](https://news.ycombinator.com/item?id=49610072)) "Agda is my first choice for proof checker and for math-y explorations" ([source](https://news.ycombinator.com/item?id=47928965)) "For proof checking I actually prefer Agda." ([source](https://news.ycombinator.com/item?id=50127360))
- Helpful interactive tooling and developer support (2 comments): "the tooling was interactive in a helpful way I've never experienced with other languages" ([source](https://news.ycombinator.com/item?id=49065033)) "These are very high level functional languages with sophisticated developer tooling." ([source](https://news.ycombinator.com/item?id=50144977))
- Elegant, beautiful language design (2 comments): "extremely elegant yet flexible mixfix notation mechanism" ([source](https://news.ycombinator.com/item?id=47926559)) "Agda and Idris are more beautiful for sure" ([source](https://news.ycombinator.com/item?id=49008556))
- Pattern matching and dependent types (2 comments): "They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear." ([source](https://news.ycombinator.com/item?id=50144309)) "I loved Agda 2 as a dependent type language" ([source](https://news.ycombinator.com/item?id=47109980))

## What people warn about

- Not practical for building software (2 comments): "I prefer agda as proof checker but its not a practical choice for building software." ([source](https://news.ycombinator.com/item?id=47927756)) "has a more proof-assistant flavor than an actual programming language flavor" ([source](https://news.ycombinator.com/item?id=49471063))
- Little training data for AI (2 comments): "It's one of the few languages I've seen that's sufficiently unrepresented in training data." ([source](https://news.ycombinator.com/item?id=47926618)) "Agda will have little training data so the result will not be nearly as good" ([source](https://news.ycombinator.com/item?id=49266622))

## Alternatives hackers recommend

- [Lean 4](https://hackerapproved.com/p/lean.md): 268 recommend
- [Rocq](https://hackerapproved.com/p/rocq.md): 25 recommend
- [Coq](https://hackerapproved.com/p/coq.md): 24 recommend
- [Isabelle](https://hackerapproved.com/p/isabelle.md): 14 recommend
- [Metamath](https://hackerapproved.com/p/metamath.md): 14 recommend

## Cite as

Hacker Approved, "Agda", https://hackerapproved.com/p/agda/ (counts from 1,795,640 Hacker News comments, November 2025 to November 2026).