Refinement Types vs Full Dependent Types: The Middle Ground Nobody Talks About HOT ★

Came here to say that F* is doing something even more interesting — it's genuinely both. It has a two-level verification story:

F* doesn't force you to choose. When SMT can handle it, you get automation. When it can't, you drop down to explicit proof terms. That's the design I actually want.

The meta-type theory of F* is also more expressive than pure refinement systems because it includes Tot, GTot, Lemma effect labels that let you reason about effects along with correctness properties.

Been saying this for years in the dependent types in industry thread. The academic community's obsession with proof terms has genuinely set back industrial adoption of formal methods by a decade.

You're not fooling yourself. Here's the actual hierarchy of what you're buying:

Level 0: No types beyond primitives. Runtime errors everywhere. (JavaScript engineers, look away.)
Level 1: Standard Hindley-Milner. Catches a lot but misses value-level constraints.
Level 2: Refinement types (LiquidHaskell, F* SMT layer, Dafny). This is where 90% of real bugs live and where automation is still feasible.
Level 3: Full dependent types (Agda, Coq, Lean). Maximally expressive, requires significant proof engineering effort.
Level 4: HoTT and beyond. Here there be dragons.

The dirty secret is that most "critical" properties — memory safety, arithmetic overflow, array bounds, protocol state invariants — fall cleanly in Level 2's expressiveness. You don't need inductive families and universe polymorphism to prove that your buffer index is in bounds.

Dafny in particular has a really compelling story here. The SMT backend (also Z3) handles most invariants automatically, and the syntax stays close to imperative code. I've introduced it to two different teams and seen real engineers actually use it within a week.

I'll be the villain. This "pragmatic sweet spot" framing papers over some fundamental issues.

Problem 1: SMT solvers are black boxes with opacity problems.

When Z3 says your program is verified, what exactly does that mean? You've established that a certain quantifier-free formula over linear arithmetic is unsatisfiable. Great. But did your refinement annotations actually capture what you wanted to prove? The spec-implementation gap is just moved to the annotation layer.

In Agda, your proof term is the proof. The kernel checks it. There's no oracle making decisions you can't inspect. When something is admitted in Agda, you see the postulate keyword staring at you. In LiquidHaskell, Z3 timeouts just... silently succeed sometimes?

Problem 2: The predicate language boundaries are sharp and ugly.

Try expressing in LiquidHaskell that reverse (reverse xs) == xs. Go on. I'll wait.

The moment you need to reason about recursive functions and their fixpoints, SMT hits a wall. reverse is not in any SMT decidable theory. You need Refinement Reflection (which LiquidHaskell now has, credit where due) but at that point you're writing explicit equational proofs anyway — you've just reinvented a weaker Agda with worse error messages.

Problem 3: False confidence. "Level 2 covers 90% of real bugs" is a claim I'd want to see rigorous support for. It's also exactly the kind of thing that leads teams to ship underspecified systems with a green CI badge.

Can I bring Dafny into this? Because I think it shows the refinement model at its most industrial-friendly. Here's a verified binary search:

Look at this. It's practically pseudocode. The requires/ensures/invariant annotations read like English. A software engineer with zero formal methods background can understand what's being verified and write these specs themselves after an afternoon of tutorials.

That's the win. It's not about what you can prove. It's about the ratio of proof engineering effort to verified properties acquired.

I concede that the Dafny example is genuinely compelling for imperative code. The loop invariant + pre/postcondition style is essentially structured Hoare logic and there's solid theory behind it.

My concerns are more about the failure modes than the happy path. Specifically:

SMT decidability cliff: everything is smooth until you hit a property the SMT can't handle, and then you get either a timeout or a spurious counterexample that you have to debug without knowing whether it's a real bug or a solver incompleteness artifact. That debugging experience is genuinely painful.

On the opacity point: I'll grant that GHC's type checker is also not fully transparent to end users. But the LiquidHaskell trusted computing base includes Z3 itself — a massive, complex piece of software. The Agda kernel is ~2k lines of Haskell. These are meaningfully different trust stories.

That said — and I want to be fair — I think F* has done the best job of genuinely integrating both worlds. The Lemma effect in F* means you can escalate from "Z3 handles it" to "I'll write a proof term" fluidly. That's the right design direction.

Real world data point: I work on a cryptographic library and we use F* (the SMT layer) for most of our verification. The properties we verify:

• Buffer bounds everywhere (zero runtime bounds checks in hot paths)
• Constant-time execution for crypto ops (modeled via taint types)
• Integer overflow/underflow for field arithmetic
• Memory aliasing conditions

All of this lives comfortably in the SMT-decidable fragment. For the handful of deep algebraic properties (commutativity of field operations, group law correctness), we write the explicit proofs. It's maybe 5% of the annotation burden.

The thing that AgdaCat is missing (I think) is that for most industrial verification targets, the hard part is not the proof difficulty — it's the annotation discipline. Getting engineers to write specs at all is the battle. Refinement types lower that barrier dramatically.

A verified crypto library with refinement types is better than an unverified one. This should not be controversial.

Something that hasn't been mentioned: the inference story for refinement types is genuinely impressive and has no analog in full DT systems.

In LiquidHaskell, most refinements propagate automatically via Liquid Typing — you often don't need to annotate intermediate expressions at all. The constraint inference fills in the gaps. Try getting that kind of inference in Agda for anything non-trivial.

The n - 1 :: Nat at the recursive site is inferred because LH has the context n :: Nat and n /= 0 from the pattern match, so n - 1 >= 0 is automatically derived. SMT handles that arithmetic implication without any user-provided hint.

This is why I say the annotation experience is fundamentally different from dependent types. In Agda you'd be passing around Fin indices or explicit proofs. Here it just... flows.

Jumping in from Team Full-DT to partially concede the point.

I've spent years in Coq and I think there's a real spectrum here that the "DT vs refinements" framing flattens. The distinction that matters most to me is proof-term verification vs. oracle-based verification:

Proof-term verification (Agda/Coq/Lean): The type checker is a proof checker. There's a tiny trusted kernel. Every claim is backed by a checkable derivation. Soundness follows from the metatheory.

Oracle-based verification (LiquidHaskell/Dafny): The type checker generates constraints and queries an SMT solver. Soundness depends on the SMT solver being sound for the fragment used AND the constraint generation being correct. That's a larger TCB.

This doesn't mean oracle-based is worse — it's a different point on the automation/trust tradeoff curve. For most engineering contexts, the SMT oracle story is fine. For high-assurance aerospace or crypto where you need formal guarantees you can independently audit, I'd want proof terms.

The real exciting thing: Lean 4 + native SMT integration might be giving us the best of both worlds. You get a kernel-checked proof, but the SMT oracle helps fill in the tedious bits automatically.

One thing I haven't seen mentioned: LiquidHaskell also handles termination checking as part of its refinement story. It's actually kind of elegant:

The / [len xs + len ys] annotation provides the termination metric — the SMT checks that this measure strictly decreases at each recursive call. You get totality proofs "for free" with a one-line hint per function, roughly.

Agda does this too obviously, but Agda's termination checker is structural and will reject things that LH accepts via well-founded metrics. Different tradeoffs.

Progress! The AgdaCat acknowledges a point. Mark this day.

I want to synthesize what I think we're actually agreeing on underneath the disagreement:

1. SMT-backed refinement types are sound for their stated properties (assuming Z3 soundness, which is extensively tested)
2. The decidable fragment is a real limitation that matters for some verification goals and not others
3. For engineering teams, the annotation UX and learning curve are decisive factors that favor refinement systems
4. For high-assurance proofs where independent auditability matters, proof-term systems give you something SMT can't
5. F* is doing something interesting by trying to dissolve this binary

The thread title says "the middle ground nobody talks about" — I'd argue this conversation is evidence that the community is starting to talk about it more. The question of where to set the verification dial for a given project is an engineering judgment, not a matter of principle.

Refinement types are not dependent types. They're not trying to be. They're trying to be useful, and for a wide class of real software properties, they succeed.