You're not wrong but you're framing it as a competition when it isn't one.

Refinement types and dependent types occupy different points on the expressiveness/automation trade-off. LiquidHaskell can verify a ton of arithmetic properties automatically by outsourcing the proof obligation to an SMT solver like Z3 — but the moment you step outside the decidable fragment of the logic, you're stuck. Dependent types let you escape that cage at the cost of writing the proof yourself.

The right analogy: refinement types are like a really smart linter that checks your preconditions automatically. Dependent types are like a proof assistant that can verify anything, if you're willing to do the work.

I broadly agree for most industry code. But "most industry code" isn't what dependent type research is optimising for. The point of Lean 4 Mathlib isn't to write fast CRUD apps — it's to formalise significant chunks of mathematics.

That said I'll concede your SMT point hard. For anything that lives in linear arithmetic, Int bounds checking, list length constraints — an SMT-backed system absolutely annihilates the manual proof approach ergonomics-wise.

I want to steelman OP's position a bit more aggressively than the previous replies have.

The thing people miss is that proof burden scales superlinearly with specification complexity. Adding a simple size constraint to your type is easy. Adding a sortedness invariant is harder. Adding a sorted, size-bounded, de-duplicated list with provably correct insert and delete is now a small research project. Composing multiple such invariants together is where things really go sideways.

There's also the issue of what I call proof brittleness. In Idris 2, a seemingly innocuous refactoring of your data structure can cascade into hours of proof repair. You didn't change the semantics at all — you just reorganised the fields of a record — and now rewrite chains don't work anymore and you have to figure out why Refl is unhappy.

-- Idris 2: what should be a trivial equality
-- becomes a painful exercise in rewriting
data SortedVec : (n : Nat) → Type where
  Nil  : SortedVec 0
  Cons : (x : Int) → SortedVec n
       → {auto ok : headGe x sv} → SortedVec (n + 1)
-- Now try to prove concatenation preserves sortedness.
-- I'll wait.

I've seen senior engineers with ML PhDs bounce off Idris 2 because the implicit argument resolution is finicky — as someone pointed out elsewhere, even a good tactic can require you to supply a bunch of additional arguments explicitly because the elaborator can't figure out what you mean.

The ergonomics problem IS the problem. Beautiful theory that nobody can use in practice is just philosophy.

Hot take incoming: the real problem isn't dependent types vs refinement types — it's that we keep trying to find one solution when the answer is obviously stratified verification.

Think about it as a pyramid. At the bottom you have your ordinary types (Rust's borrow checker, Go's nil safety, whatever). One layer up, refinement types with SMT discharge handle arithmetic and shape constraints with near-zero proof overhead. At the top, for the 5% of code that is truly safety-critical and structurally complex, you break out full dependent types.

This is basically what F* does! You have SMT-dischargeable VCs for most things and you can drop into manual proofs when you need them. Steel and Pulse for separation logic, full dependent types for the gnarly stuff. The Tot / Ghost / Lemma / ST effect layering is actually a really elegant answer to the "how much verification do you want" question.

(* F* effect system lets you choose your verification budget *)
val safe_div : x:int → y:int{y <> 0} → Tot int
let safe_div x y = x / y
(* SMT handles the precondition automatically at callsites *)
(* No manual proof lemma required *)

The frustrating thing is that F* is still kind of a niche tool and most people in industry don't know it exists. Meanwhile everyone's trying to use Lean 4 for everything because Mathlib is impressive and it has good marketing.

Coming at this from a research angle: I think the original post conflates "dependent types are not the answer to everything" (true) with "dependent types are not worth the effort" (false for the domains they're designed for).

In my thesis work (verified compilation of a DSL for distributed systems), full dependent types in Agda let me prove properties that would be literally impossible to express in a refinement type system — for example, proving that two separately compiled modules, when linked, preserve a global invariant about message ordering. The types need to talk about the relationship between program structure and semantic behaviour, which requires computation in types.

Refinement types are restricted dependent types. A refinement type { x : A | P x } is literally a Σ-type where the predicate is restricted to a decidable fragment. The restriction buys you automation. That's a great trade if your problem lives in that fragment!

But my problems don't, and I suspect a lot of critical infrastructure verification problems don't either. seL4 wasn't verified using LiquidC for a reason.

Can we talk about the universe polymorphism situation for a moment because nobody mentions this when they're evangelising dependent types to beginners.

In Lean 4, Agda, and Coq, you have this whole universe hierarchy to prevent Russell-style paradoxes. Type 0 : Type 1 : Type 2 : ... etc. For most code it's invisible. For library-level generic code — the kind where you're abstracting over types of types — it becomes a genuine headache. You start getting universe constraint errors that are almost impossible to debug without a deep understanding of the metatheory.

-- Lean 4: universe polymorphism becoming visible
universe u v
def myFunctor.{u, v} (F : Type u → Type v) : Type (max u v + 1) := ...
-- "Why is the universe max+1??" — every Lean 4 newcomer

This is a solvable problem with experience but it represents a genuine onboarding cliff. When I'm trying to convince my employer to adopt a verification tool, "it requires deep knowledge of Martin-Löf type theory to write generic library code" is a tough sell.

Agda at least has universe polymorphism that's slightly more transparent in my experience, but it's still a lot.

Hard SMT enjoyer checking in. I want to make a point about decidability that I think gets glossed over.

The reason refinement type systems backed by SMT are so ergonomically pleasant is that the verification is fully automated within their fragment. You write the spec, the checker runs, you get a yes/no answer with no interaction required. This is what LiquidHaskell gives you for most real-world Haskell properties — the paper showed it could prove 96% of recursive functions terminating with roughly 1.7 lines of termination annotations per 100 lines of code. That's an incredible ratio.

With dependent types, even with great tactics, you're in an interactive loop. You write a partial proof, inspect the goal state, apply a tactic, inspect again. It's powerful and I respect it, but let's not pretend it's the same workflow. For a team that needs to verify things and ship code, the interactive proof loop has real costs.

True. And ALSO the seL4 proofs took approximately 11 person-years of expert verification effort for roughly 10,000 lines of C. That's a data point about cost, not just capability. I love seL4. I would not recommend the seL4 approach for a fintech startup's authentication module.

Real talk: we are also sleeping on GADTs as a middle ground that nobody talks about in this debate.

GADTs in Haskell or OCaml give you a significant chunk of dependent type expressiveness — phantom type parameters that track runtime-relevant structure, existential types, index-enforced state machines — without requiring you to commit to a full proof assistant. Most type-state patterns that people reach for dependent types to implement can be handled with GADTs + smart constructors + a bit of newtype discipline.

-- Haskell: type-state with GADTs, no proof terms needed
data Connection (s :: State) where
  Closed :: Connection 'Closed
  Open   :: Handle → Connection 'Open

send :: Connection 'Open → ByteString → IO ()
close :: Connection 'Open → IO (Connection 'Closed)

This is expressible, readable, and requires zero familiarity with Martin-Löf type theory. A junior Haskell dev can understand this type-state pattern in an afternoon. Getting to the same place with Idris 2 indexed types would require a week of ramp-up minimum.

The ladder of verification commitment goes: untyped → simple types → GADTs/phantom types → refinement types → full dependent types. Most industrial code has no business being above step 4.

I want to bring up something nobody has mentioned: proof maintenance cost.

Even if you successfully verify a module with full dependent types, you're creating a maintenance liability. Every time the API changes, every time the data structure evolves, every time a business requirement shifts the invariant — your proofs break. And not in a way that's easy to fix; it's not like a type error where the compiler tells you exactly what to update. Broken proofs can be deeply confusing to fix, especially if the original author has left the team.

This is an under-discussed cost in the academic literature, which tends to present verification as a one-time effort ("we verified X!") rather than an ongoing engineering commitment. The Mathlib project actually does a lot of work maintaining proofs across Lean version upgrades and refactors — but Mathlib has dedicated contributors and institutional support. Most industry teams don't have that.

I'm starting to believe this more than I'd like to admit as someone who spent three months last year doing nothing but proof repair after a library refactor. It's not a fun job.

That said: I still think for protocol implementations, cryptographic primitives, and OS-level code, the investment pays off. The question is whether your codebase is more like seL4 or more like a typical web backend. If it's the latter, please consider just writing good tests and using property-based testing before you commit your team to Idris 2.