Fail-closed LAWS — Bend s01

Install. Guide. One trivial law. Break it. Watch the checker refuse. Name one gap.

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

Install Bend. Print the guide. Write one trivial law. Break it on purpose. Watch the checker refuse the merge. Name one gap the law never covered.

§I — Frame

Asr session 01 for Bend. First live fire of the Bend experiment track. Week 1 fire 1. Home folder: . Primary live cite: https://bend-lang.com/. Vendor org: https://higherorderco.com/. On-disk hub (path for citations): .

This is an experiment / laws-gate lesson. It is not a factory pitch. Hedronite primary-stack law stands: Rust + TypeScript for full-stack work; Python + Nix for ops and config. Bend does not join that daily clock. A teammate banked the incorporation shape on 2026-09-19: WATCH plus a named disposable spike. Session 01 teaches the spike DoD, not product adoption.

Done-criteria: you can state install → guide → one trivial law → deliberate break fails closed; you can name one incompleteness gap (host, IO, @unsafe, renderer, or install friction).

§II — What the gate actually is

Vendor contract on bend-lang.com:

1. Humans (or agents) declare invariants in LAWS.bend.
2. Proofs live in PROOF.bend.
3. Before commit, run bend PROOF.bend (or the documented check command of the day).
4. A change that breaks a stated law fails closed.

LAWS.bend is the precise sibling of an AGENTS.md rule list, with a checker behind it. The checker only verifies properties you wrote. Unstated policy is free to rot. That single sentence is the whole of the honesty required for this track.

§III — Install gate (a teammate §4 steps 1–2)

On a disposable host only (tower or Bot-VM shape; not a mesh-wide PATH without a separate lab go-ahead):

curl -fsSL https://bend-lang.com/install.sh | sh
bend --version
bend guide

If bend --version does not print, stop. File the miss. Stay on WATCH. Do not invent a workaround install for the lab Mac or citadel in this lesson.

If-then-thus: if the binary is missing after the install script, then the spike fails at step 1, thus you bank friction and do not pretend the laws gate exists on that host.

§IV — One trivial law (named technique: Law Pin)

Yagyu names the cut once. Law Pin: write the smallest property that must never break, then force a counterexample.

Vendor game demo (shape from bend-lang.com):

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

Toy alternate when you are not building a game (sorted non-decreasing):

# LAW: sorted output is non-decreasing.
law sorted_nondecreasing:
  for xs: List<U32>
  ys = sort(xs)
  nondecreasing(ys) == True{}

PROOF.bend holds the discharging proof the model (or you) writes. Session 01 does not teach proof tactics. Session 01 teaches ownership: you own the law; the checker owns the refuse.

§V — Deliberate break fails closed

Keep a green bend PROOF.bend. Then edit the implementation (or ask a model to "make the board wrap around" in the game demo) so a stated law no longer holds. Re-run:

bend PROOF.bend

Expect a non-zero exit / explicit fail. That refuse is the product of this lesson. If the checker stays green after a law-breaking edit, you found a toolchain gap: bank it under incompleteness, do not call the spike a pass.

Musashi declarative: the gate that does not refuse is not a gate.

§VI — Incompleteness checklist (required name-one)

Laws cover stated properties only. Outside the statement, verified wrong products still ship. Checklist for the done-criterion:

1. Host / OS — files, permissions, packaging, PATH, launchd, containers.
2. IO / network / secrets — TLS, sockets, wallets, API keys (usually unencoded in LAWS).
3. **@unsafe / FFI** — escape hatches the checker may not treat as law surface.
4. Renderer / JS edge — UI and browser side effects sit outside game-board laws (vendor notes already warn here).
5. Install / maturity friction — young toolchain; expect bugs; native matrix is prove-on-spike.

Name one gap from that list in your own words before you close the session. Example sentence: "This law never constrained filesystem writes, so a green PROOF.bend still allows a bad host write."

§VII — AGENTS.md rhyme (without fleet reseat)

Vendor suggests adding to AGENTS.md:

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

For Hedronite: keep that block inside a disposable Bend project only. Do not paste it into Rust/TS/Python product AGENTS files as a primary-stack replace. The rhyme is real; the reseat is forbidden by curriculum law.

§VIII — Common mistakes

1. Treating a green proof as "do not read any code." You still author and review laws.
2. Adopting Bend as the software-factory language for Hedronite shipping crates.
3. Skipping the deliberate break, so you never saw fail-closed.
4. Running the install on citadel/apiary scratch without GO.
5. Comparing "superior to Lean" as a category win; different jobs (out of scope here; a teammate already graded the overclaim).

§IX — Boundaries

• Not Lean tactics training.
• Not CUDA/Metal performance theater.
• Not curriculum clock reseat.
• Not Lapis / Facet / HedronDB / Geode rewrite.

§X — Close

Session 01 is the gate demo: install, guide, one law, one refused break, one named incompleteness gap. Next unmarked: session 02, laws depth (who owns which properties).

Related:

On a disposable host, run the five a teammate §4 steps once. Stop when the checker refuses your deliberate break, write the gap you named, and leave Bend off the primary stack.