Open Laws and Live Evidence in Bend 2

Bend's core checker returned normally for a law stating that zero equals one. The law had no implementation, and the checked book recorded one open claim. Trying to fill it with reflexivity failed. Trying to use an unfilled declaration as live evidence also failed.

Those results describe different stages of checking. A proposition can be well formed without being proved. The CLI closes that distinction by rejecting a book whose open count is nonzero. An integration that calls only the lower-level validator needs to preserve that completion check.

I examined revision 295e996574573e3a88827b1cf7045b437333c8f0, whose CLI declares version 2.0.39. I ran the unchanged TypeScript checker module directly with Node 24.19.0 on Linux, using synthetic local Bend files. I did not run the Bun CLI, the compiler's native backends, or the Lean-based proof kernel. These tests establish behavior of the examined checker, not its formal soundness or advertised performance.

A Law Starts as a Declaration

Bend combines dependent types, affine resource use, and a compiler with native and JavaScript targets. Its implementation is concrete: bend2/bend.ts contains parsing and checking, comp.ts contains compilation and runtimes, main.ts owns the CLI, and safe.ts translates checked books for a separate kernel. The repository also contains a base library and executable .bend test fixtures. The package configuration is small; the checker module used here imports Node built-ins.

The language guide proposes separating human-owned laws from the implementation and proofs a coding agent edits. That can make a specification more precise than a prose request, but the repository still needs a gate that distinguishes a declaration from completed evidence.

This synthetic file declares an impossible equality without supplying a proof:

import Base
law unfinished:
  {0n == 1n : Nat}

I passed it through book_load() and book_valid(). Validation returned without an exception, with book.hols === 1. There was no proof of the equality. The checker had accepted the shape of the open proposition and recorded the remaining obligation.

The validator implementation processes declarations and definition events in order. A declaration is visible before its body becomes available. Unchecked bodies do not unfold during checking, and a live reference to an unfilled definition is refused.

That last restriction matters. An agent cannot resolve an obligation merely by naming another unproved law and treating it as established evidence.

Filling the Body Changes the Question

In another fixture, I supplied {==} as a proof of {0n == 1n : Nat}. The checker rejected it with this diagnostic:

Error:
- expected : 0n
- observed : 1n
Location: impossible
4 | def impossible():
5>|   {==}
  |   ^^^^
6 |

Reflexivity did work for {n == n : Nat}. I also checked an inductive proof of addition's right-zero property:

import Base
law right_zero:
  for n: Nat
  {Nat.add(n, 0n) == n : Nat}
def right_zero(n):
  match n:
    case Zero{}:
      {==}
    case Succ{p}:
      %h@right_zero(p) : {Succ{Nat.add(p, 0n)} == Succ{_} : Nat}; {==}

That file checked with an open count of zero. The successor case uses the recursive proof on p to rewrite the equality goal. The location of the rewrite placeholder matters: my first attempt put it on the other side and produced a different goal that the checker rejected. The version above is the one executed successfully in the published probe.

These are deliberately small properties. They demonstrate proof checking and useful error feedback without claiming that an agent implemented a real application correctly. A checked property is still only the property that the file states.

Seven Files Through the Actual Checker

The replay probe verifies SHA-256 digests of bend2/bend.ts and bend2/base.bend, then imports the original checker. It writes seven temporary fixtures and calls the real loader and validator on each fresh book. It does not replace parser or type-checker logic.

Obtain those two files from the pinned revision, preserving their paths. From the portfolio checkout, I ran:

node public/blog/bend-open-laws/checker-probe.mjs /tmp/bend-note26

The command exited zero. Its zero-hole gate is an explicit reproduction of one criterion in the CLI's book_read() function. It is not the full CLI verdict, which also checks dependencies and can invoke the separate kernel.

Fixture	Core result	Open count or diagnostic
Reflexive equality	Checked	0
Inductive right-zero proof	Checked	0
Reflexivity offered for zero equals one	Rejected	Expected 0n, observed 1n
Law with no body	Checked as open	1; zero-hole gate blocked
Proof body containing ?TODO	Checked as open	1; zero-hole gate blocked
Definition reads an unfilled law	Rejected	Live reference requires a filled definition
Unfilled law named U32.unproved is used	Rejected	A base-like name did not provide evidence

Selected stdout:

reflexivity: checked; open_count=0; zero-hole gate=pass
inductive_right_zero: checked; open_count=0; zero-hole gate=pass
false_equality: rejected; expected diagnostic matched
unfilled_law: checked; open_count=1; zero-hole gate=blocked
todo_body: checked; open_count=1; zero-hole gate=blocked
live_unfilled_reference: rejected; expected diagnostic matched
base_like_name: rejected; expected diagnostic matched
PASS: 7 synthetic checker cases; no CLI verdict or Lean kernel claim

The upstream tests include open claims, live use of an unfilled law, and TODO bodies. I inspected them; I did not run the cluster-oriented repository gates or claim a full suite pass.

The CLI Adds Completion and Trust Checks

The examined book_read() calls the validator and then rejects a nonzero book.hols. It also requires a file named PROOF.bend to import a neighboring LAWS.bend when that laws file exists. These are source-inspected safeguards around the checker API.

The cli_verdict() adds a dependency check. It traces reliance on @unsafe and foreign definitions through types, bodies, and datatype declarations outside Base. With the kernel option enabled, it also calls the separate verifier. Thus, zero open obligations is a necessary criterion, with further trust conditions beyond the counter exercised by my probe.

The guide documents --verdict as rechecking translated proofs with a Lean-proven kernel. It also states that the translation itself has no proof. I did not validate that kernel, its trusted assumptions, the translation, or the CLI's dependency traversal here.

For an agent workflow, this makes the validation contract fairly specific. Preserve the laws being checked, reject incomplete books, and choose the intended verdict mode rather than interpreting a successful low-level function call as a complete proof result. The tested core refused false reflexivity and live unfilled evidence; the surrounding CLI supplies additional gates that an embedding would otherwise have to retain.