# Hole Driven Development

> Use when implementing in a language with typed holes (Haskell, Lean 4, Rust) where a compiler provides hole diagnostics — runs the compiler loop autonomously

- Skill: `jhhuh/hole-driven-development` (Agent Skill)
- Install (CLI): `npx skillmds@latest add jhhuh/hole-driven-development`
- Raw SKILL.md: https://api.skillmd.com/api/skills/jhhuh/hole-driven-development/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: jhhuh (https://skillmd.com/u/jhhuh)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/jhhuh/hole-driven-development

---


# Hole Driven Development — Compiler Loop

**REQUIRED BACKGROUND:** `hole-driven-development-core`

## Overview

Drive implementation through the compiler's typed hole diagnostics. Write holes, compile, read what the compiler tells you, fill one hole, repeat until it compiles.

**Core principle:** The compiler is the oracle. Every fill decision is grounded in diagnostics, not memory.

## When to Use

- Source file has typed holes (`_`, `_name` in Haskell; `sorry` / `_` in Lean; `todo!()` in Rust)
- A compiler is available that reports hole diagnostics
- You're implementing against a type signature

## The Compiler Loop

```
1. Write type signature + stub with hole(s) in the file
2. COMPILE — run the compiler
3. READ diagnostics: expected type, bindings in scope, valid hole fits
4. PICK the most constrained hole (fewest valid fits)
5. FILL exactly one hole — guided by diagnostics, not memory
   - If the fill is complex, introduce sub-holes
6. VERIFY semantic correctness against previously filled holes:
   - Does shared state flow correctly between this fill and prior fills?
   - Are resource scopes (locks, handles, channels) consistent?
   - Do error paths compose correctly?
   The compiler catches type errors but not logic bugs.
7. COMPILE again — go to 3
8. When compilation succeeds (no holes remain):
   REVIEW-ALL — re-read the complete implementation holistically:
   - State transitions that span multiple fills
   - Resource acquired in one fill, released in another
   - Error paths that cross fill boundaries
   - Loop invariants depending on multiple fills
   Fix any systemic bug the per-hole VERIFY could not catch.
9. EXIT
```

**One hole per compile cycle.** Fill one, compile, read. Do not batch-fill.

**Use named holes.** When introducing multiple holes:

- **Haskell:** Use `_name` (e.g., `_base`, `_recursive`) instead of bare `_`.
- **Lean 4:** Use `sorry` with a preceding comment (e.g., `-- HOLE: base case` then `sorry`), or bind with `let _base := sorry`.
- **Rust:** Use `todo!("hole_name")` (e.g., `todo!("base_case")`).

Named holes make diagnostics easier to read and holes easier to track across compile cycles.

**Diagnostics over memory.** Even if you "know" the answer, compile first and let the diagnostics confirm or correct you. The compiler may reveal constraints you missed.

**When NOT to decompose further.** Some algorithms are inherently monolithic — dual-cursor walks, complex FSMs, coroutine-style loops. If the state machine's transitions are tightly coupled, keep it as one hole with internal structure via comments. The compiler catches type errors at hole boundaries but not logic bugs from split state.

## Compiler Invocation

Auto-detect from project structure:

| Language | Hole syntax | Compile command | Detection |
|----------|------------|-----------------|-----------|
| Haskell | `_`, `_name` | `cabal build` if `.cabal` file exists; otherwise `ghc <file> -fno-code` | `.cabal`, `.hs` |
| Lean 4 | `sorry`, `_` | `lake build` if `lakefile.lean` or `lakefile.toml` exists; otherwise `lean <file>` | `lakefile.lean`, `lakefile.toml`, `.lean` |
| Rust | `todo!()` | `cargo build` if `Cargo.toml` exists; otherwise `rustc <file>` | `Cargo.toml`, `.rs` |

When using `nix develop`, prefix commands: `nix develop -c <compiler> ...`

## Autonomy

Run the loop autonomously. **Stop only when:**

- **Done:** Compilation succeeds, no holes remain, and REVIEW-ALL found no systemic bugs.
- **Ambiguous:** Multiple equally valid hole fits and no constraint distinguishes them. Surface the options to the human.
- **Stuck:** 5+ compile cycles on the same hole without progress. Ask for help.

## Reading Diagnostics

### GHC (Haskell)

GHC's typed hole output gives you:

1. **Found hole: `_ :: <type>`** — what type the hole needs
2. **Relevant bindings** — what's in scope with types
3. **Valid hole fits** — expressions that type-check in this position

**Use all three.** Valid fits narrow the search. Relevant bindings show what you can compose. The expected type is the constraint.

**Beware misleading fits.** GHC may suggest a value that type-checks but is semantically wrong (e.g., `z` instead of a recursive call). Cross-reference with the function's purpose.

### Lean 4

Lean 4's `sorry` and `_` output gives you:

1. **Unsolved goals** — the expected type for each `sorry` or `_`
2. **Context** — hypotheses (variables and their types) available in scope
3. **Expected type** — the target type the hole must produce

**`sorry` vs `_`.** `sorry` silences the error and allows compilation to continue — useful for incremental HDD. `_` forces the elaborator to infer and report what's needed. Prefer `sorry` for skeleton stubs, switch to `_` when you want the elaborator to narrow the type.

### Rust

Rust's `todo!()` compiles successfully (it satisfies any return type via `!`), so diagnostics come from type mismatches in surrounding code, not from the hole itself. To get useful diagnostics:

1. **Replace `todo!()` with a wrong-type expression** (e.g., `()`) to force a type error showing "expected X, found ()"
2. **Read "expected ... found ..." messages** — these tell you the hole's required type
3. **Check "help" suggestions** — rustc often suggests methods, trait implementations, or conversions

**Rust holes don't report like GHC.** Since `todo!()` has type `!` (never), it type-checks in any position. You won't get "valid hole fits." Instead, rely on the surrounding type context and intentional type mismatches to extract constraints.

## Red Flags — STOP

- Writing implementation without compiling first
- Ignoring compiler diagnostics ("I know the answer")
- Filling multiple holes between compile cycles
- Skipping compilation after a fill ("it's obviously correct")
- Looping on the same hole without trying a different approach

**If you catch yourself doing any of these: STOP. Compile. Read. Then proceed.**