Incompleteness checklist drill — Bend s03

Walk the four gaps. Green proofs cover stated laws only.

<!-- hal:authoritative:yaml -->

Walk four gaps aloud. Keep the green checker bound to stated laws. Refuse the sentence that treats silence as coverage.

§I. Frame

Asr session 03 for Bend. Third live fire of the Bend experiment track. Week 2 fire 1. Home folder: . Primary live cite: https://bend-lang.com/. Vendor org: https://higherorderco.com/. On-disk hub: . Gap prior: a teammate 2026-09-19 incorporation note () for incompleteness only. Fair secondary: bend2.dev notes that board laws do not cover a JS renderer.

Session 01 shipped fail-closed install and one named gap. Session 02 assigned Law Own and Cover Bound. This session drills the checklist so you can walk it cold.

Done-criteria: you can walk a short incompleteness checklist (host, IO, @unsafe, renderer/FFI) and say a green proof does not cover unstated gaps.

Still experiment lane. Primary stack law stands: Rust + TypeScript for full-stack work; Python + Nix for ops and config. Bend does not join that daily clock. Do not re-run the curl installer as the body of this lesson.

§II. Why a checklist (named technique: Gap Walk)

Yagyu names the cut once. Gap Walk: before you trust a green PROOF.bend, name the surfaces the laws never mentioned.

Vendor pitch is strong: declared laws, discharging proofs, checker refuse. That pitch stays true only inside the stated surface. A teammate’s incorporation note grades “don’t look at the impl” as overclaim for Hedronite hosts: unstated policy, host, IO, renderer, FFI, and @unsafe sit outside unless you wrote them as laws.

Musashi declarative: silence in LAWS.bend is not a theorem. It is an open edge.

§III. The four-box checklist

Walk these four boxes every spike. Speak one concrete risk per box.

1. Host / OS. files, permissions, packaging, PATH, launchd, containers, disk. A board law never bound rm -rf on the vault.
2. IO / network / secrets. TLS, sockets, wallets, API keys, clipboard. Green game proofs do not mint key custody.
3. **@unsafe / FFI**. escape hatches and foreign calls the checker may not treat as law surface. Name the hatch if the spike uses one.
4. Renderer / FFI UI edge. browser or JS side effects outside board laws. bend2.dev already warns that game-law coverage does not extend to the renderer.

Optional fifth for later sessions (friction log, not today’s done-criteria): install / maturity friction on a young toolchain. Bank it when it bites; do not confuse it with property coverage.

If-then-thus: if a property never appears in LAWS.bend, then a green checker cannot have verified it, thus treating green as product-safe is a category error.

§IV. Cover Bound, drilled

Cover Bound (session 02) again, now as a drill script:

1. Open LAWS.bend. List every law name.
2. For each name, write one sentence: “This covers ___.”
3. Run Gap Walk on the four boxes. Write one sentence per box that starts with “Unstated:”.
4. Only then run bend PROOF.bend (or the documented check of the day).
5. On green, say aloud: “Green covers the listed laws only.”

Invert steps 1-4 and you rubber-stamp a discharge of unknown properties. That is still wrong when CI is green.

§V. Worked drill (you_cant_win)

Vendor-shaped law:

# LAW: no move sequence leads to victory.
law you_cant_win:
  for moves: List<Move>
  board = replay(start(), moves)
  is_won(board) == False{}

Checklist answers for this spike (fill your own words; keep this shape):

Green PROOF.bend for you_cant_win means victory stays impossible under the checker’s board semantics. It does not mean the host write policy is safe. Session 01’s example sentence still holds: the law never constrained filesystem writes, so a green proof still allows a bad host write.

§VI. Sentences you must refuse

Refuse these mergespeak lines:

• “Don’t need to read the impl; it’s verified.”
• “Green means the product is safe.”
• “Host gaps are covered because the board law is green.”
• “Bend replaces AGENTS.md for the fleet.”

Replace with:

• “Verified for the laws we wrote.”
• “Green means stated properties held under today’s checker.”
• “Host gaps stay open until written as laws.”
• “Bend is an experiment lane; Rust+TS / Python+Nix clocks stand.”

§VII. Common mistakes

1. Skipping Gap Walk because yesterday’s proof was green.
2. Collapsing all four boxes into “maturity” so nothing stays actionable.
3. Re-teaching install instead of walking gaps.
4. Turning this into a Lean superiority debate (out of scope).
5. Closing with a primary-stack reseat toward Bend.

§VIII. Boundaries

• Not install tutorial (session 01 already).
• Not Law Own re-teach beyond naming Cover Bound as prior.
• Not Lean tactics training or Lean smackdown.
• Not software-factory adoption for Hedronite shipping.
• Not curriculum clock reseat.
• Not Maghrib quiz×4 (Maghrib stays quiz×3 on the Dhuhr trio).

§IX. Close

Session 01 showed refuse. Session 02 assigned ownership. Session 03 drills Gap Walk: host, IO, @unsafe, renderer/FFI, then the Cover Bound sentence that green does not cover silence. Next unmarked: session 04, checker friction log.

Related:

Open a LAWS.bend (vendor demo or yesterday’s spike). Fill the four-box table with one Unstated line each, say the Cover Bound sentence aloud, and stop.