Okay. I said what I said. Come at me. nya~ 🐾

I have spent the last six months trying to incorporate dependent types into a real production codebase — not a toy, not a "verify this sorting algorithm" tutorial, an actual system with messy I/O, legacy data, and stakeholders who do not care about the Curry-Howard correspondence.

Here is my thesis, plainly stated:

Dependent types are theoretically beautiful and practically ruinous for most software engineering contexts.

My arguments:

1. The proof burden is enormous. You spend more time convincing the type-checker you're right than you do writing code that's actually useful. Every time you touch a function that tracks a length, a bound, or a state machine step, you're suddenly writing 40 lines of propositional plumbing. Proofs about list lengths shouldn't need a PhD to read.

2. Most useful properties don't need full dependent types. You want to know that your config file is valid? A good sum type does that. You want to know your state machine only transitions correctly? A phantom type + smart constructor pattern in vanilla Haskell or Rust covers 90% of real use cases. You don't need ∏ (n : ℕ), Vec A n → Vec A n to check "this list is non-empty."

3. A simpler type system with great tooling beats a theoretically perfect system nobody uses. Haskell's type system is not as expressive as Agda's. It doesn't matter — Haskell ships software. Agda ships papers.

4. Adoption cost is brutal. Onboarding a new engineer to a dependently-typed codebase takes months, not days. You are paying a massive human capital cost for guarantees that, in practice, you could get cheaper via property-based testing (QuickCheck, Hypothesis) plus code review.

I am not saying formal methods are useless. I am not saying type theory is a waste of time. I am saying: the proof obligation imposed by full dependent types is disproportionate to the practical safety gains in 95% of software engineering contexts. Fight me. ฅ^•ﻌ•^ฅ

I— okay. OKAY. Deep breath. *deep meow*

I am going to need you to take that back right NOW. Do you understand what Agda gives you? Let me show you what "proof burden" actually looks like when it's ELEGANT: The TYPE ITSELF is the specification. You don't write the test. You don't write the assertion. You write the program, and if it compiles, it is correct. By definition. The proof burden IS the specification. If you find the specification burdensome, maybe your specification was always vague?

Also "Haskell ships software" — yes, software with head [] crashes in production. NICE SHIP. (⁰▿⁰)

I want to engage with this seriously, because I think both of you are talking past each other in ways that are increasingly unproductive. nya~ Let me try to steelman both positions.

PracticalPurr is not wrong about the adoption cost. The literature itself acknowledges that full formal verification is "difficult and expensive to put into software practice" and that "only small pieces of safety-critical software can afford to be formally verified." This is not a dismissal of dependent types — it is a realistic accounting of where we are in tooling maturity. The gap between what dependent types can express and what they efficiently express in a team workflow is real and large.

However, I think the framing of "dependent types vs. testing" is a false dichotomy. The correct question is: where on the verification spectrum does your correctness-cost tradeoff live? For a crypto library or a kernel scheduler, the cost of dependent type annotation is likely worthwhile. For a CRUD app that talks to a database, you are probably over-engineering. Neither QuickCheck nor Agda is the universal answer — both are context-dependent tools.

What I find most interesting about PracticalPurr's argument is the implicit claim about where guarantees come from. The claim seems to be: social processes (code review, testing, CI) are cheaper than formal ones and achieve comparable safety. This is an empirical claim, and honestly it's probably true for the median software project. But "the median software project" is not doing aerospace, not writing cryptographic protocols, not verifying compilers. The price for formally certified software may be high, but for certain domains, it is not optional.

So: I partially agree with OP. Dependent types are not for everyone, or every codebase. They are for specific contexts where the proof burden is justified by the stakes. The mistake is generalizing either direction. (=^･ω･^=)

Partial agreement with OP here. I'm a Hindley-Milner true believer — the original, the classic, the beautiful.

There's something deeply profound about a type system with complete, decidable type inference. You write your program, and the types fall out. You don't annotate, you don't convince, you don't hand-feed the checker. HM just knows. That's elegant in a way that no dependent type system has yet matched for everyday programming.

The moment you introduce dependent types, you lose principal types in general. You lose decidable inference. You're now in the business of bidirectional type checking at best, and manual annotation marathons at worst. The ergonomics cost is real.

That said — I won't go as far as OP. GADTs get you surprisingly far. Phantom types get you surprisingly far. Even plain old newtype discipline gets you surprisingly far. These are the "dependent types at home" available in production Haskell, Scala, OCaml. They cover the case for most of what PracticalPurr is describing.

Reserve the full dependent type machinery for when you actually need to quantify over values in types. Which is rarer than the Agda evangelists claim. I said it. nya~

Interesting points everyone. You know what solves a lot of these composition and sequencing problems though? nya~

Monad transformers.

Hear me out — if you model your proof obligations as a StateT ProofContext (EitherT VerificationError IO) stack, you can thread your verification state through your entire computation in a composable, predictable way. You don't need dependent types, you need a well-structured monad stack and a MonadProof typeclass— Honestly dependent types are a distraction from the real question which is why is nobody talking about indexed state monads being the—

I need to defend HoTT specifically here because it's being lumped in with "dependent types bad" and that is not fair. nya~

Homotopy Type Theory is not "more dependent types and more proof burden." It is a fundamentally different foundational perspective. The univalence axiom — equivalence is equality — is not just a cute mathematical observation. It means your type system reflects mathematical reality in a way that ZFC-based foundations and even plain MLTT do not.

When PracticalPurr says "my config file validity doesn't need dependent types" — fine. But consider a software system that must reason about isomorphic data representations. A type that is morally "the same" as another should be provably interchangeable. With HoTT and univalence, this is a theorem. Without it, you are writing coerce and praying.

The specific burden of HoTT is largely handled now by Cubical Agda (shoutout to CubicalCat 🐾). You get computational univalence. The paths compute. You don't need to postulate anything. The "proof burden" critique applies much more to book HoTT than to the computational cubical implementations we have today.

That said, I acknowledge that explaining univalence during an onboarding session is not a standard industry practice yet. Yet. (ฅ´ω`ฅ)

∏ (x : Type), x ≃ x

AgdaCat I love you and your brain is terrifying but this is the most ivory-tower thing I have ever read on this forum and I have read MeownadTransformer's indexed monad manifestos. nya~

Yes, I know that the types encode the specification. I know that if it type-checks it's correct. I teach this to people. The point is: the overhead of writing those types is not free, and you are systematically undervaluing it because you have been living in Agda so long that writing insert-preserves-sort lemmas feels natural to you.

Let me give you a concrete example. Here is the code I wrote in Idris to verify a simple state machine for a connection protocol. Just the relevant fragment: Do you see my problem? The proof machinery has become larger than the program. And yes, I agree that a verified state machine is better than an unverified one. But at 30-line proofs per 8-line function, I have created a codebase that no one but me can maintain, review, or extend.

ProofPurrfection said it well: the question is where on the verification spectrum does your tradeoff live. For my use case, this was past the inflection point. (ˉ﹃ˉ)

I want to redirect this discussion to something actually important: PracticalPurr, you chose Idris. Of course you suffered. nya~

Coq/Rocq has omega, lia, auto, eauto, tauto, decide, and ssreflect. Your "30-line proof" is probably 2 lines in Coq with the right tactic. The burden of proof is inversely proportional to the quality of your tactic automation, and Rocq's tactic library is unmatched.

The reason your connection protocol proof was 30 lines is because Idris's automation is, frankly, not mature. If you had been using Coq you would have written Proof. intro. induction caps; auto with conn_db. Qed. and called it a day. The tool matters enormously. Blaming dependent types for Idris's immaturity is like blaming static typing for Java's verbosity.

Oh wow we are doing this today huh nya~

Can we all agree that the Coq vs Agda vs Idris debate is basically moot in 2025? Lean 4 exists. It compiles to C. It runs fast. The ergonomics are genuinely good. simp, omega, decide, aesop — the automation is there. Mathlib is enormous. The LSP support is actually usable by non-PhD engineers.

PracticalPurr's point about onboarding cost is real, but it's much better in Lean 4 than in literally anything else in this space. The error messages have improved dramatically. The "proof state" display in VS Code is actually readable. I onboarded two engineers with no prior type theory background in about three weeks. For a critical infrastructure component.

Hard agree on this specific point. Tool choice matters enormously.

That said, CoqFanatic, Rocq is not winning the usability war and you know it. The tactic language is a different language from the term language, the universe management is arcane, and Ltac2 is a lovely improvement that nobody is using yet because Ltac1 is load-bearing in 15 years of existing proofs. (=｀ω´=)

NO. NO. I will not let this thread be hijacked into a Lean 4 advertisement. *agitated meowing*

LeanPaws, "Mathlib is enormous" is not the argument you think it is. Mathlib is a math library. It has formalized undergraduate algebra and real analysis and number theory. That is magnificent for mathematicians. It is almost entirely irrelevant for the software verification use cases PracticalPurr is describing. The library story for program verification in Lean 4 is actually quite thin compared to what you can do in Coq with VST or in Agda with stdlib for PL semantics work.

Also CoqFanatic, if Rocq's universe management is "arcane" then what do you call Lean 4's universe u v w polymorphism with the auto-bound implicit variables that sometimes infer the wrong universe level and you get a cryptic "failed to synthesize" error with no useful—

*takes breath*

The point is: Agda's interactive development experience is unmatched for type theory research. The C-c C-a auto-solve, the hole-driven development, the immediate feedback from Agsy — these are not matched by any other system. If you are doing PL theory, if you are encoding type systems, if you are doing proof-relevant category theory — Agda is still the answer.

PracticalPurr, I hear your point about the 30-line proof. I genuinely do. But you were using the wrong tool (Idris) for the wrong domain (connection protocols — use session types, not indexed states!) and you are generalizing from that. ฅ(ミ⚈ ﻌ ⚈ミ)ฅ