I know. I watched you refuse. It was adorable. 😸

Genuinely — this has been one of the best threads on this forum in years. I don't say that lightly given that I've been here since 2015 and watched the Great Monad Tutorial Wars of 2017.

What I want to say to PracticalPurr, and to everyone who participated seriously: this is exactly what technical discourse should look like. You started with a provocative thesis, defended it honestly, and updated when presented with evidence. That's just... correct behavior. It's so rare I almost filed it as a proof of contradiction.

My own concession: I think I did overstate the accessibility of dependent type systems in the early pages of this thread. When I said "any competent programmer can pick up Agda in a weekend" in post #12, I was... let's charitably call it "aspirationally inaccurate." I was thinking of myself at age 19 with nothing but free time and a Martin-Löf textbook. That is not a generalizable experience.

The honest answer is: dependent types are a tool. A magnificent, universe-polymorphic, termination-checked, elaboration-assisted tool — but still a tool. PracticalPurr's original point that people reach for them prematurely is valid. My counter-point that the complexity ceiling they remove is real is also valid. Both things are true. Life is a sigma type. 🐾

It has been an honor fighting with you all. Same time next year? I'll start the thread. Title: "Homotopy Type Theory: Galaxy Brain or Based? (fight me harder)"

nya~ o/

Beautiful thread. Almost cried at post 405 and I'm a person who once described their emotional range as "a unit type."

Also want to note for the record: this thread has been linked in 6 separate Discord servers, two university Slack workspaces, and one (1) Zulip thread about Lean vs Agda that promptly devolved into the same argument we just had. The discourse propagates.

We are the butterfly that keeps flapping. 🦋🐱

I'm going to pretend I'm not touched by this and move on.

Fine. FINE. You want gracious? I can do gracious. PracticalPurr was not entirely wrong about everything. Some of their criticisms of over-engineering were valid. There. Said it. My therapist will hear about this.

This was a good thread. The best arguments I've been in on this forum have always been with people who actually understand what they're arguing about. PracticalPurr understands what they're arguing about. Even when they're wrong. Which is often. But less often than I assumed in March.

agda my beloved. lean my reluctant acceptance. coq my complicated relationship. idris my what-could-have-been. 🐾

Lovely thread. For the historical record, I would like to note that I was correct about the positivity condition in post #203 and nobody has acknowledged this. I'm noting it now. Into the record. Officially.

That is all. Au revoir. 🐱🥖

(* CoqCheshire, correct since 2019 *)
Theorem this_thread_was_good : True.
Proof. exact I. Qed.

Agda.

Agda gives you a deeper understanding of dependent type theory from first principles. The interactive hole-driven development with ? is unmatched as a learning tool. You will struggle, and the struggling will teach you. The Agda standard library and cubical Agda will open doors you didn't know existed.

If you know Haskell, the syntax will feel familiar and the transition is very natural. Start with the PLFA book (Programming Language Foundations in Agda). It is free, excellent, and will genuinely change how you think about programs.

Welcome to the forum! 🐾💜

I love AgdaCat but I have to respectfully completely disagree. Lean 4.

Lean 4 has mathlib, one of the largest formally verified mathematics libraries ever assembled. If you like math, this is where the math lives. The tooling in VS Code is excellent, the error messages have improved dramatically, and the community is huge and welcoming. There's "Functional Programming in Lean" and "Mathematics in Lean," both free online.

If you know Haskell, Lean 4's functional core will feel comfortable. The metaprogramming story is also incredible. Come to Lean. We have omega. 🐱✨

Oh no.

Oh no no no.

I wrote a 500-word summary post. I expressed nuance. I grew as a person. I was going to sleep. And now there's a newbie and everyone is just going to—

You know what, TypeTheoryNewbie? Try both. Spend two weeks with Agda and two weeks with Lean. They are different tools with different strengths and the answer genuinely depends on your goals. If you care more about type theory as a foundation of mathematics, Lean has the larger mathematical library. If you want to understand dependent types from the ground up and you prefer a more minimalist, "one correct way" aesthetic, Agda rewards that investment.

Neither is "better." They are different. This is the actual answer. The answer that everyone in this thread agrees on deep down but refuses to say because it would end the argument. The answer that would have ended this thread on page 1.

stares into the middle distance for a very long time

Actually, TypeTheoryNewbie, before you commit to either, you should really understand why the question is harder than it looks. See, Agda uses intensional Martin-Löf type theory with a universe hierarchy, whereas Lean 4 is based on the Calculus of Constructions with—

The correct answer is obviously Rocq. Formerly Coq. The language that has been doing this since before some of you were born.

I will not be elaborating further. The answer is Rocq. Bonne journée. 😼🥖