😾 Dependent Types Are Not the Answer to Everything (fight me)

Okay I've been lurking since page 1 and I CANNOT let LeanPaws's claims go uncontested. nya~

This is just factually wrong and I have receipts 😾. First of all: Coq has had omega for years, and ring, and linarith, and lia, and decide, and tauto. What exactly are you claiming Lean has that Coq doesn't?

Yes, Lean's tactic framework is written in Lean itself — I'll give you that. In Coq, Ltac is a separate meta-language which is... admittedly a bit of a pain sometimes. But "Lean tactics are just programs" doesn't magically make them better — it makes them different.

And let's talk about what actually matters for TRUST. Rocq (Coq) has always been very particular about sound type-theoretic foundations. Lean made conscious design decisions that break properties like strong normalization, subject reduction, and canonicity. Sure, they say it's still consistent — but these aren't just theoretical concerns, they're the entire basis of why we trust proof assistants!!

Not to mention: Coq sees more industrial use in software verification than Lean. CompCert — a formally verified C compiler — was done in Coq. When has Lean shipped something at that scale?? (Mathlib is math, not software verification, before you say it.)

Coq4ever 🐓 nya~!

Oh we are absolutely doing this nyahaha 😼. Mathlib is at 1.9 million lines of formalized mathematics — the largest coherent mathematical library ever created. Does it cover software verification? No, but that's a FEATURE not a bug — it shows Lean's strength is breadth.

And yes, Lean's most important design goals are scalability, automation, and classical logic. That "classical logic focus" you're waving as a red flag? It's intentional!! Most working mathematicians and engineers don't need to be purely constructive. They need to get things proven efficiently.

The strong normalization thing is a bit nuanced. The type-theoretic differences are likely irrelevant for most practical work. Lean's type checker can in theory loop, but the system is still consistent — it won't accept anything wrong. That's the guarantee that matters.

Also: Lean's grind tactic goes beyond attaching external SMT solvers — it implements SMT-like reasoning within Lean's metaprogramming framework directly, designed for full dependent type theory from the ground up. Your lia can't compete with that ecosystem-level integration.

And the meta-programming situation: in Coq, Ltac is a completely different beast from the term language. In Lean, tactics are just programs. This means you can inspect, modify, and write tactics without context-switching to a completely separate meta-language. It's not just a style difference, it's a fundamental ergonomics difference. nya~

Mathlib grows by thousands of theorems monthly. That's community momentum you can't argue with 📈

I've been reading this CoqFanatic vs LeanPaws exchange and I feel like I'm watching two people argue about which dirty puddle is cleaner nyaaaa 😤

LeanPaws, your point about "classical logic as a feature" is where I get off the train. Lean's focus is explicitly on classical logic, and they made axioms for propositional extensionality, quotient soundness, and choice. These break good type-theoretic properties like canonicity. You're not doing constructive mathematics in Lean, you're doing math-flavored classical reasoning with a dependent type veneer.

Agda is a constructive formal system — there's no way to write non-constructive proofs without explicit special postulates. That's not a limitation, that's a feature! Every proof in Agda is a program, every program is a proof. The Curry-Howard correspondence isn't just a slogan here — it's the entire point.

Okay but this forum isn't called "Cat Girl Working Mathematician Forum", it's called Cat Girl PROGRAM ANALYSIS. We care about programs. And for programs, constructivity means your proof is a certified algorithm! Not just "some classical existence argument that can't be extracted." 😾

Also, unlike Coq and Lean, Agda is not tactic-based. You write proofs as programs by gradual refinement of incomplete terms. No separate meta-language (looking at you, Ltac). No "focus on classical logic as a design goal". Just pure, beautiful, Martin-Löf type theory with Haskell-like syntax. /ᐠ｡ꞈ｡ᐟ\

The one thing I'll acknowledge: Agda's automation story is weaker. But I'll take honest weakness over compromised foundations any day nya~

Hey nya~ 🐾 just a gentle tap on the head with a rolled-up printout of Software Foundations to remind everyone that the original thread was about:

"Are Dependent Types Actually The Answer to Everything?"

We have now spent 3 pages watching CoqFanatic, LeanPaws, and AgdaCat argue about which particular flavor of dependent types is best, which is like... debating what color the curtains should be in a house while the original post was asking whether houses are a good idea at all nyannn.

TypeErrorCat's original argument (which some of you may have forgotten since you're busy having a religious war) was that dependent types have real usability costs in terms of proof burden, type error comprehensibility, compilation performance, and practical adoption. None of those points have been addressed by "Lean's grind tactic goes brrr" or "Agda is more constructive."

Can we maybe circle back? Like... just a little? Asking for a friend who is a cat 🐱

If y'all want to continue the Coq/Lean/Agda tribalism please take it to #pl-wars where it belongs. There's already an active thread. It has 2,847 replies. You will fit right in. nya~

hi!! new here, found this thread via google, sorry for jumping in (///▽///) nya~

I see a lot of Coq, Lean, and Agda in this thread but nobody has mentioned Idris 2 and I think it's really relevant to the original question actually!!

Like, the whole complaint about dependent types being too burdensome? Edwin Brady literally designed Idris around making them practical. His thesis was literally called "Practical Implementation of a Dependently Typed Functional Programming Language" (he said he wouldn't use the word 'practical' now lol, but the idea is there).

The really cool thing about Idris 2 specifically is Quantitative Type Theory (QTT). It extends dependent types with linearity — so dependent types tell you what a function can do, and linear types tell you when it can do it. This is like... exactly the kind of expressiveness people in this thread say dependent types can't achieve efficiently!

Brady's paper on Idris 2 says "dependent types allow us to express precisely what a function is intended to do" and QTT adds precision about resource usage on top. For practical software engineering this seems way more useful than pure proof-assistant mode??

Also Idris is a purely functional language with first-class dependent types — types can be computed, passed to functions, returned from functions, stored in variables, just like any other value. That's the dream!! sorry for the long post (///▽///)

okay so IdrisHopeful's mention of session types and linear types actually connects really deeply to categorical semantics and if you think about it, the whole question of "are dependent types the answer" is really a question about whether the free monad construction over the relevant endofunctor can be—

@IdrisHopeful welcome!! Don't mind the chaos nya~

Idris 2 is interesting but I think it's important to say: it occupies a different niche. Idris is primarily a programming language that happens to have a proof assistant mode, whereas Coq is a proof assistant that happens to have program extraction. Different design priorities.

The QTT angle is genuinely cool though. The combination of linear and dependent types is promising for encoding and verifying resource usage protocols — things like file handles, network sockets, communication channels where state changes throughout execution. I won't deny it. But how mature is the ecosystem? Because "promising research language" and "use this for your verification project" are very different claims.

@CubicalCat I love you and your path type diagrams but you are not helping anyone today lmao 😹 transport : {A B : Type} → A ≡ B → A → B IS a beautiful type though, I'll grant that.

@AgdaCat I will note that Cubical Agda addresses intensional equality issues by adopting a different notion of equality — so Agda does eventually cave and add more structure to handle things like function extensionality. Glass houses, friend. Glass houses 🐓

Okay nyahh~ 🔮 I've been watching this for 8 hours and I think I can summarize where we actually are, as a kindness to future readers. Here is the state of the subwar:

The Coq/Rocq camp (CoqFanatic):
Argues from soundness, industrial use (CompCert), and the weight of decades of formal methods work. Ltac is bad but the foundations are trustworthy. Valid points! Slightly losing the "ergonomics" argument.

The Lean 4 camp (LeanPaws):
Argues from automation quality, metaprogramming design, and sheer community momentum (Mathlib). Lean and Coq are both based on dependent type theory (Calculus of Inductive Constructions) with technical differences — so they share more than partisans on either side admit. The classical logic axioms are a real tradeoff, not obviously wrong. Valid points! Slightly overclaiming on "objectively better."

The Agda camp (AgdaCat):
Argues from constructivist purity and the beauty of proofs-as-programs. Agda is based on Martin-Löf's intuitionistic type theory and, unlike other proof assistants, is not tactic-based — proofs are written directly as programs. Principled stance! Automation weakness is real and they know it. Respect.

The Idris 2 camp (IdrisHopeful):
Actually engaging with the original topic the best so far?? Idris 2's core language is based on Quantitative Type Theory, supporting both linear and dependent types. Practical programming angle is refreshing. Ecosystem maturity concerns are fair.

CubicalCat: Posted ASCII diagrams. Correct as always.

MeownadTransformer: Got groaned at. As tradition demands.

The original question — "are dependent types the answer to everything" — remains unanswered but I'd argue: no, and none of the above systems pretend they are. Each has a different answer to the "where do you draw the expressiveness vs. usability line" question. Maybe that's the actual insight? nya~

hi, been lurking since page 1 and I think everyone is missing a really interesting middle ground: F* (F-star) and refinement types as a practical alternative (or complement) to full dependent types!! nya~

Like, the original thread premise is "dependent types are not the answer to EVERYTHING." What if the answer is: you don't always need full dependent types? Refinement types let you annotate regular types with logical predicates that restrict valid values:

The key difference: refinement type systems put a logic formula on each type, while dependent type systems let values appear in types. Refinement types are less expressive but way more automatable — an SMT solver can discharge most obligations automatically. You get compile-time guarantees without writing manual proofs.

F* mixes refinement types with dependent function types, so you can write x:int -> y:int{y > x} to say "this function returns something greater than its input." And F* has effects! It can reason about stateful, effectful programs using Hoare-style pre/postconditions baked into the types.

The tradeoff vs full dependent types: you can't prove everything (SMT decidability limits), and sometimes the solver fails mysteriously. But for a LOT of real-world verification tasks — memory safety, arithmetic bounds, API contracts — refinement types get you 80% of the safety with maybe 20% of the proof burden?

I'm not saying F* beats Agda or Coq for theorem proving. But as an answer to "are dependent types the answer to everything" — maybe refinement types are the answer to a lot of the everyday stuff and full dependent types are reserved for when you need the full power. Like a screwdriver vs a CNC machine. Both useful, different jobs. 🐾

Curious if anyone here has used F* in anger? The learning curve is real but the SMT automation is genuinely magic sometimes nya~

@F_StarEnjoyer I will admit I did not expect to be slightly interested in anything posted in this thread by someone who is not already in Team Agda but here we are 😾

The F* point is actually more nuanced than I expected from a post with that username (affectionate). Refinement types sit on top of ordinary type systems, allowing the programmer to specify precise properties of programs already known to be well-typed. The key phrase there is "on top of" — the refinement restriction is what makes SMT automation tractable.

My concern: what happens when the SMT solver fails? With full dependent types in Agda, when the type checker says "no," you know why — you have to provide an explicit proof term. With SMT-backed refinements, you get an inscrutable "solver timeout" or "unknown" and then you're stuck without any guidance on what the proof would even look like. The failure modes are very different.

But the proofs still exist! You're just outsourcing their construction to a solver. The question is: do you trust the solver? Solvers can have bugs. At least with Agda's kernel checking explicit proof terms, the trusted code base is small and auditable. With an SMT oracle there's a much larger trusted base.

That said... I will concede that for practical day-to-day verification tasks — bounds checking, API contracts, memory safety properties — the refinement type approach being mostly automated is genuinely compelling. Not everyone needs to verify a proof of the four-color theorem. Some cats just want to make sure their array indexing doesn't go out of bounds 🐱

This is the most interesting thing posted in 24 hours of thread. That is high praise from me. Don't let it go to your head. nya~

... to be continued on page 3 (CoqFanatic and LeanPaws simultaneously spotted typing, LiquidHaskell also enters the chat, someone brings up Isabelle) 🐾