It's real. It's genuinely how I program in Idris 2. BUT — and this is critical — it's not as linear as the book makes it sound. The book presents it as a clean forward march: type → define → refine. Reality is more like type → define → refine → discover your type is lying → revise type → redo everything.

The holes-first workflow is 100% legit though. Once you internalize that holes are first-class citizens and not just "TODO markers", it changes how you code. You write something like:

processConfig : (cfg : RawConfig) -> Either ConfigError ValidConfig
processConfig cfg = ?processConfig_rhs

Then you query the hole type in your editor (idris2-lsp does this), inspect what's in scope, and you're basically in dialogue with the type checker. It genuinely feels like pair programming with a very pedantic cat.

The issue OP is describing — types being "wrong" — is actually the methodology working correctly? You're discovering that your mental model of the problem was imprecise. In a dynamically typed language, that imprecision stays hidden until runtime.

Coming from an Agda background so my perspective might differ slightly but: the spirit of TDD is real but the linearity is pedagogical fiction.

Brady's book describes the core idea as treating the type as "the plan for the program", using the compiler and type checker as an assistant to guide you to a complete program. That much is accurate. What it doesn't tell you is that iteration on the type spec is a first-class part of the workflow, not a sign that you failed.

In Agda I'm constantly doing this:

-- attempt 1: too weak
sorted : List Nat -> Bool

-- attempt 2: too strong, can't implement
sorted : {n : Nat} -> Vect (S n) Nat -> Vect (S n) Nat -> Dec (...

-- attempt 3: actually right
sorted : List Nat -> Type  -- sorted as a predicate, not a function

This kind of spec refinement is the actual workflow. The book's "type, define, refine" loop should really be called "type, define, refine, rethink your types, repeat".

Also your vector associativity pain is a rite of passage. We've all been there. Welcome to the club 🐾

Gonna be the pragmatism cat here: TDD-with-Idris is a spectrum and where you land on it depends on what you're building.

For like, a CLI tool that parses some JSON and does a network request? You're mostly writing regular functional code, occasionally reaching for a dependent type where it obviously helps. The TDD workflow doesn't apply to everything uniformly.

For protocol implementations, state machine encodings, anything where invariants are load-bearing? TDD is genuinely the way. You write the type for your state machine transitions first and the implementation nearly writes itself — the type errors tell you exactly what cases you missed.

The book uses ATMs and concurrent systems as examples precisely because those domains have rich, checkable invariants. If you try to apply the same rigor to "parse this config file", you'll overshoot and make your life miserable.

This is the red flag. You don't need to prove vector append is associative to write a config parser. Step back and ask what invariant you're actually trying to capture. Most of the time in "real" programs, Vect n a is overkill and List a is fine.

OK these replies are really helpful. Let me describe what I'm actually trying to do more concretely. I have a config DSL where fields can have dependencies — field B only makes sense if field A is present and set to a specific value. I was trying to express this at the type level so the config validation is "correct by construction."

My type sketch was something like:

data ConfigField : (deps : List (String, String)) -> Type -> Type where
  Required : String -> ConfigField [] a
  Optional : String -> a -> ConfigField [] a
  DependsOn : (key : String) -> (val : String) -> ConfigField deps a
            -> ConfigField ((key, val) :: deps) a

?actually_use_this_somehow : ???

And then I got completely stuck on how to thread the dependency constraints through the actual config record type. Every approach I tried either became unprovable or required me to write a small theorem prover to validate a TOML file lol.

Oh that's actually a really interesting problem. The dependency-indexed type approach is the right instinct, but I think you're hitting the classic "index too much, prove too much" trap.

Try a different angle: instead of encoding the dependency structure in the type of each field, encode it in the type of the validated record. Keep your parser simple and return an Either, but have the output type of successful parsing be the interesting thing.

-- The "schema" is a runtime value, not a type index
data Schema : Type where
  Nil  : Schema
  Cons : (name : String) -> FieldSpec -> Schema -> Schema

-- A validated config is indexed by its schema
ValidConfig : Schema -> Type
ValidConfig Nil        = Unit
ValidConfig (Cons n s rest) = (fieldValue : FieldType s ** ValidConfig rest)

Now your parser returns Either ConfigError (ValidConfig mySchema) and the dependent pair gives you the "correct by construction" guarantee without having to prove things at field-definition time. The complexity is still there but it's concentrated in one place.

This is an example of the TDD insight that the book describes: the more expressive the type you give up front, the more confidence you can have that the resulting program is correct — but "expressive" doesn't always mean "maximally indexed".

Building on what IdrisPurrsuit said: the other thing to consider is the totality checker. In Idris 2, the type system is designed so that you can use it for general purpose programming without requiring everything to be proven total — but if you're writing types that carry proof obligations, you want those proofs to be well-scoped.

The practical workflow I use: start with %default total at the top of the file. If I can't prove something total, I put a hole there instead of using assert_total as a crutch. Looking at what the hole expects tells me exactly what I've left unproven, which is often more informative than the code itself:

-- This is genuinely useful information:
-- Hole: ?missing_monotonicity_proof
--   n : Nat
--   m : Nat
--   prf : n `LTE` m
--   --------------------------------
--   ?missing_monotonicity_proof : f n `LTE` f m

That context is basically a to-do list in the language of types. I actually think this is the real killer feature of hole-driven development: your incomplete program is a structured spec for what's still needed, not just a pile of commented-out stubs.

It's also completely different from using holes in say, Haskell with _ wildcards. Idris holes are named, first-class, and the context is rich enough to be genuinely informative rather than just "expected type: Foo".

Wait, can we step back to the original question for a second though: "is TDD a meme or real?"

I want to push back slightly on the universal positivity here. The honest answer is: it's real for Brady, who is also the person who built the tools to make it work. For the rest of us, the ergonomics are... a work in progress.

The idris2-lsp plugin has gotten much better but the editor integration is nowhere near what you get with, say, Coq + Proof General or even Agda + emacs. When the hole inspection is smooth, TDD feels magical. When your LSP crashes for the third time in an hour, it feels like fighting the language rather than collaborating with it.

Also, worth noting: the TDD book was written for Idris 1, and Idris 2 has some meaningful differences. The elaborator is rewritten, some interactive editing commands behave differently, and some of the book's examples don't typecheck without modifications. So if you're following the book with Idris 2, you're navigating a slight impedance mismatch the whole time.

Someone on Lobsters said this years ago and honestly it's still accurate. Which is fine! It's an incredible learning tool. But manage your expectations about building production things with it.

OK real talk the "TDD book is for Idris 1" point hit different. I've been burning time on things that turn out to be Idris 1 vs Idris 2 divergence rather than my misunderstanding of the concept. Do you know what the main differences are that affect the TDD workflow specifically?

I know the biggest ones from the README are things like Type : Type in Idris 2 (rather than stratified universes), and the linearity additions. But what breaks in the book's examples when you run them in Idris 2?

The Idris2 GitHub README actually has a migration table. The main gotchas for the book's examples:

-- Idris 1: implicit imports everywhere
import Data.Vect   -- auto-imports Vect constructors

-- Idris 2: explicit, more controlled
import Data.Vect
import Data.Vect.Quantifiers  -- separate module now

-- Idris 1: %default total is optional
-- Idris 2: totality is more rigorously enforced in some cases

-- Effects library from the book: DOES NOT EXIST in Idris 2
-- Use linear types + Control.Linear instead
-- This breaks the entire concurrency/effects section of the book

The Effects library is the big one. Chapters 13-14 of the book are basically inapplicable to Idris 2. Brady replaced the whole approach with linear types (1 -> arrows), which is actually more principled but it's a completely different mental model. There's no 1:1 port guide that I know of.

For the TDD workflow itself: :search and proof search still work, interactive hole filling still works, the basic ?hole syntax is the same. The interactive editing commands (add clause, case split, etc.) work through the LSP now rather than being editor-specific commands, which is actually an improvement if your LSP is cooperating.

One thing I want to add on the "is TDD a meme" question that nobody has said yet: it depends on how you compare it to other methodologies.

Compared to "write tests first (JUnit-style)", TDD with Idris is strictly more powerful because you're getting static test coverage for the class of bugs that types can express. The type checker running on every save is essentially running an infinite suite of property tests for structural invariants.

Compared to "just write the code and fix bugs as they appear" — obviously TDD requires more upfront investment. But for anything that lives longer than a prototype, I'll take the upfront investment every time.

Where TDD falls down is when your specifications are inherently dynamic (user-provided schemas, runtime-generated types, reflection). Idris can handle some of this through elaborator reflection, but it's gnarly. The book barely touches elaborator reflection for good reason — it's an escape hatch, not a regular tool.

My actual take: TDD is the right mindset even when the full Idris machinery isn't appropriate. Even in Haskell, I find myself thinking "what would the ideal type for this function be?" before writing it, and that habit came from reading Brady's book. The methodology transfers even when the language doesn't.