23. Working in Hanki as an agent - the loop

The tooling below is one loop, not disconnected flags: sketch the program with typed holes and let hanki check dictate each gap; learn the surfaces you call from hanki doc --format=json and hanki query instead of reading source into context; close diagnostics with *explain → --fix → re-run* rather than re-deriving edits; test with hanki test --format=json (property tests for ∀-claims, --deterministic for actor code); run just-written code under the allowance hanki effects reports, via --allow/--deny; and before landing a change to a module others consume, let hanki api-diff classify the contract delta. HANKI-CARD.md §22 carries the same loop in compact form - the version every scaffolded project's agent reads. The bullets below are the per-tool depth:

• Diagnostics carry stable codes. A coded diagnostic prints as error[H####]: - e.g. error[H0601]: call requires effect …. The code is an opaque, append-only handle (H + four digits, grouped by compiler phase: H00xx lexer, H01xx parser, H02xx–H05xx checker, H06xx effects/throws); the prose message carries the meaning, the code is only a stable lookup key for tools and agents. One registry holds every code, and a test pins them - a shipped code's number and title never change or get reused. Not every diagnostic is coded yet: the lexer, parser, and effect/throws families are; the rest of the checker is being filled in.
• --format=json gives structured diagnostics. hanki check and hanki build default to the human prose above. Pass --format=json and they instead emit one versioned envelope to stdout: {"schema": "hanki-diag-v1", "diagnostics": [{code, severity, span:{path,start,end}, message, rendered, fixes}]}. code is the H#### string or null for an uncoded diagnostic; span is byte offsets into path; message is the bare text and rendered is the full file:line:col: error[H####]: … line, so an agent reads prose without re-deriving it. A clean check emits an empty diagnostics array; exit code is unchanged (non-zero on any error). JSON is the only structured encoding - the binary cbor form was dropped as having no consumer (a Hanki-native consumer would reuse the same envelope with a swapped encoder). In JSON mode stdout is exactly one envelope; build progress (wrote/linked) moves to stderr.
• fixes are machine-applicable edits. Each diagnostic carries fixes: [{span:{path,start,end}, replacement, applicability}] - the exact source edit that resolves it. span is the byte range to replace (start == end is a pure insertion), in the same file as the diagnostic; applicability is machine-applicable (always correct), maybe-incorrect, or has-placeholders. Today the effect-propagation families emit them: H0601 (call needs an effect the action doesn't declare) and H0604 (a throw with no matching throws row) attach the precise […]-row patch - widening an existing row or inserting a fresh one after the return type.
• hanki check --fix applies fixes to the working tree. It writes every machine-applicable fix straight to the source, then re-checks and repeats until the cascade settles: adding [net] to an action surfaces the same need one caller up, so a chain of N actions converges in N rounds, no agent re-derivation. Edits are minimal, canonically-spaced text-span replacements; once the cascade settles, --fix runs the formatter over each file it changed to normalize it (apply-then-format). The formatter preserves comments, so your comments survive the pass. Diagnostics needing human judgement are left untouched and reported as usual. This collapses the agent loop from parse → re-derive → patch to run → re-run.
• hanki explain <code> is the recipe for a code. hanki explain H0601 prints the code's title, a canonical explanation, and the fix recipe; hanki explain (no argument) lists every code. So the agent loop reads end to end: a failed hanki check prints error[H####], hanki explain H#### says what it means and how to fix it, and hanki check --fix applies the machine-applicable ones. That one registry is the single source of truth for code, title, and explanation, so they cannot drift.
• hanki query answers "what is this?" at a source position - query semantics instead of reading files into context. hanki query FILE --at LINE:COL (1-based line and byte column; or --byte N) prints the hover answer for the identifier there: the declaration signature - effect row included - or the binder's name: type, plus defined at file:line:col. It is the LSP hover/definition surface as a one-shot command, no session needed. --format=json emits one hanki-query-v1 envelope to stdout: {"schema": "hanki-query-v1", path, byte, hover: {span:{start,end,line,col}, contents} | null, definition: {start,end,line,col} | null} - contents is the same fenced signature, hover: null means nothing identifier-like sits at the position (exit stays 0 in JSON mode; text mode exits 1 on a miss).
• hanki doc --format=json is the API surface as data - read signatures instead of grepping source. hanki doc FILE --format=json emits one hanki-doc-v1 envelope on stdout: {"schema": "hanki-doc-v1", path, module_doc, items: [{name, qualified, kind, anchor, signature, effects, doc, has_doctest}]} - every documentable symbol with its rendered signature, written effect row (["io", "throws SendFailed"]), doc prose as Markdown, and whether the doc comment carries a runnable example. anchor matches the Markdown output's {#anchor}, so the two views cross-reference. The symbol filter narrows items the same way it narrows the Markdown (hanki doc FILE map --format=json); a filter miss is an empty items array at exit 0 (text mode exits 1), mirroring hanki query's null-hover convention. So learning a module's signatures is one structured read, not a grep over its source.
• hanki api-diff classifies an API change as breaking or compatible - check the contract before you land it. hanki api-diff FILE [--against REF] (default HEAD) diffs the module's public API surface - every non-_ top-level item: signatures, effect rows, struct fields, sum variants, trait methods, impl existence, effect ops, actor handlers - between the working tree and the same path at a git revision, and classifies every delta against the locked rule table in [docs/design/api-diff.md](docs/design/api-diff.md). Purely mechanical signature analysis: an effect added to a row is breaking for under-permissioned callers (F4), T → Result<T, E> is breaking (F3), a sum variant added breaks exhaustive matches (V1), an effect removed is a compatible widening (F5); parameter renames and variant reorders are informational. Spelling never false-positives: types compare structurally after qualification (open option + Option ≡ option.Option) and generic/effect-variable names normalize positionally (<T, U> ≡ <A, B>). Text mode prints breaking: list.map: effect added to row: [] -> [io] (F4) per finding plus a trailing verdict; --format=json emits one hanki-apidiff-v1 envelope ({schema, against, verdict, counts, findings: [{rule, verdict, audience, symbol, kind, before, after, detail}]}) - before/after are rendered signatures, so narrating a delta is a template over rule + detail. Exit code is 1 on any breaking finding (informationals never affect it), so CI gates on it directly. A path absent at the ref diffs as a first release (all compatible-added). Scope (v1): single-file modules, signature-level only - a behavior change behind an unchanged signature is invisible by charter.
• Property tests catch what a single example misses. Write test "name"(x: i32, …) with typed parameters and the runner samples each from its Arbitrary instance over many seeded cases (§20) - categorically stronger than one chosen example, and especially valuable for an agent because a failing case hands you the offending input, shrunk to a minimal still-failing one. The body is the ordinary assert!; @property(cases:, seed:) tunes the count and fixes the seed. Reach for one whenever a property should hold for all inputs - a round-trip (decode(encode(x)) == x), an invariant, commutativity - not just for a chosen value.
• hanki test --format=json gives structured test results. Default hanki test prints the N passed, M failed summary and FAIL lines. Pass --format=json for one hanki-test-v1 envelope on stdout: {"schema": "hanki-test-v1", "summary": {passed, failed, stdlib_passed}, "tests": [{name, status, origin, failure?}]}. A failed test carries failure: {location:{path,line,col}, message, rendered, expected, actual, counterexample}. For a compared assert!(lhs CMP rhs), actual is the structurally-rendered lhs and expected the rendered rhs (named fields/variants for structs and sums); both are null for a non-comparison assert or any other failure. counterexample carries a failing property test's input - its sampled parameters rendered name = value and joined, shrunk to a minimal still-failing case - and is null for a plain (non-property) test failure. The rendered field is the human FAIL line. A pre-test compile error still reports as text - use hanki check --format=json for structured diagnostics; --format=json here governs only the test results.
• @encapsulated lets pure-context code use a local mutable accumulator. When a def is genuinely externally pure but wants a BytesBuilder or similar empty-effect-row action internally (building bytes, content-hashing, a comptime helper), mark it @encapsulated (§6) instead of giving it a ! and forcing the effect onto every caller. The checker verifies the mutation never escapes, so the def stays callable from meta, where-invariants, and other pure code. Reach for it only when a normal pure def won't do - most pure code needs nothing.
• ??? is a typed hole for spec-first development. Write ??? for any expression you have not filled in yet. hanki check reports, for each hole, the type the surrounding context expects and the effect budget permitted there, as a hole[H0250] advice line (severity hole on the --format=json envelope). Holes are non-blocking - a holey program type-checks, runs, and builds - but a hole reached at runtime diverges like crash! (crash: hole reached, exit 252). So an agent can sketch a program's shape, run hanki check to have the compiler dictate each gap's type and effects, and fill the holes to fit (§6, Typed holes).
• --deterministic makes actor programs replayable - use it to verify concurrent code. hanki run --deterministic and hanki test --deterministic fix the actor interleaving to a seeded schedule: same source + same inputs + same seed ⇒ byte-identical output. That turns output-diffing into a reliable verification for concurrent programs - run once, change the code, run again, diff the bytes. --seed N (implies --deterministic) explores a different interleaving, so checking a program under several seeds probes schedule-dependent bugs; when one seed fails, that seed is the exact reproduction recipe. A schedule where every actor is blocked is a deterministic deadlock: hanki run reports it on stderr and exits 251 instead of hanging, and under hanki test --deterministic the deadlocking test records one failure and the suite continues - each test runs on a fresh scheduler, so one wedged test cannot poison the next. Caveats in §6 (Debugging & observability): external inputs must be fixed for byte-equality, and OS-level rendezvous between actors is outside the gate's view. Both tiers: an AOT-compiled binary takes the same replay through HANKI_DETERMINISTIC=1 / HANKI_SEED=N in the environment, and a given seed reproduces the same interleaving on hanki run and the native binary alike.
• hanki effects answers "what would --allow need" before the program runs. hanki effects PATH prints the program's capability surface - every effect it can perform when run, the exact set the --allow/--deny gate enforces - with the rows that declare each one (io: Logger.log!, main! / net: provide Database). Declaration-level and sound: by the effect discipline every performable capability is declared in some action/handler/provide row, so the union over those rows bounds the program, over-approximating only by dead code that still declares a capability (which a capability audit should treat as live anyway). --format=json emits one hanki-effects-v1 envelope: {"schema": "hanki-effects-v1", entry, capabilities: [{name, builtin, sites: [{symbol, path, line}]}]} - builtin distinguishes the OS atoms from user-declared effects, sites are the declaring symbols with locations. A pure program prints (no capabilities) / an empty array. So the sandbox loop is: hanki effects to see the surface, then hanki run --allow <that set> to pin it. --sys switches to the OS seam itself: call-graph reachability over the compiled program from its entry, listing every reachable sys.* intrinsic (one per line; --format=json emits a hanki-effects-sys-v1 envelope {schema, entry, intrinsics, loads_modules}). Its precision contract: it over-approximates - a listed intrinsic may be dynamically dead (a fn taken as a value counts as callable; a spawned actor contributes all its handlers) - and never under-approximates within the compiled program; the one hole is module.load!-ed source, which is compiled at runtime and therefore flagged (loads_modules / a trailing caveat line) rather than analyzed. Where the declaration view reports a dead [net] action's capability, --sys omits the unreachable sys.tcp_listen! behind it.
• --deny / --allow sandbox a run by its effects - execute just-written code safely. hanki run --deny net,fs refuses to run if the program can perform a denied effect; hanki run --allow io refuses unless every effect it can perform is in the allowlist (hanki test takes both flags identically). Capabilities are the effect atoms io/net/fs_read/fs_write/db/process/time/env/random (with fs an alias expanding to fs_read+fs_write, so --allow fs_read is a read-only filesystem; [db] is a distinct intent-level atom for the database seam - the sqlite intrinsics charge [db], never the general-purpose [fs] seam (fs.read!/fs.write!), so --allow db --deny fs reaches a database but not arbitrary files, and a :memory: database - which touches no file at all - carries [db] where [fs] would be wrong. A file-backed database's own file is opened by the native engine through the [db] seam; that [db] stays a genuine "database, not the filesystem" boundary only because the seam is secured against file-reach escapes - ATTACH to arbitrary paths, loadable readfile/writefile extensions, a permissive VFS - see stdlib/extra/sqlite.hk) and any user-declared effect; --deny wins over --allow, an unknown atom is rejected, and the bare default permits everything a program does itself (its own execution is unchanged — with one runtime refinement for programs that load code, below). The check is static - it reads the already-computed effect rows and refuses before the program starts, exit code 1 with capability denied: on stderr, at zero runtime cost - and whole-program, so an effect performed only inside a spawned actor's handler is caught even where it never surfaces in main's own row. Under hanki test / hanki fuzz the surface also covers what the test blocks themselves perform: a test body carries no declared effect row of its own, so its performed capabilities are collected from the actions it calls and folded into the enforced set - a test that writes the filesystem is refused under --deny fs_write exactly as main would be, while a test that only reads is still permitted (the precise capability, not a blanket fs). So an agent can run or test code it just generated under a least-privilege allowance and have the compiler refuse anything outside it, by construction.

The allowance also travels into the runtime: every module.load! / module.reload! re-enforces it against the loaded file's declared surface - same declaration-level semantics as the launch gate - and refuses a widening load with a catchable ModuleLoadError, so runtime-loaded code cannot escape the sandbox (bytecode tier). Default-deny for loaded code: even with no --allow/--deny, a program that loads modules at runtime pins its load-boundary allowance to its own declared capability surface, so a loaded module may perform only what the host itself advertised - a dependency understating its manifest simply cannot execute the undeclared effect (capability denied: in the caught ModuleLoadError). Because a host charges the effects of every Module<T> action it calls (§14), the host's surface is the ceiling it grants loaded code: to let a plugin do net, the host declares net on the trait method it calls - which also means --deny net on the host stops the whole composition, no capability-leak hole. This bites only at the load boundary; a program with no module.load! site keeps the unconstrained fast paths (cache, unbounded fuel) untouched, and an explicit --allow is the user's deliberate allowance that replaces the derived baseline. Bytecode tier (the AOT-embed loader passes no capability policy yet, so its loaded modules are still ungated - a tracked tier-parity gap).

Capabilities bound what a run may do; a companion bound caps how much: hanki run --max-steps N faults the run (exit 250) once N bytecode steps total across every actor are spent - the run can never execute more than N; steps are metered in small per-actor grants, so with several actors running at once the fault may fire marginally early, and a single-actor or --deterministic run trips exactly at N - and a sandboxed run (any --deny/--allow) applies a generous default budget when --max-steps is unset, so untrusted code can neither perform an undeclared capability nor spin forever. hanki run --max-bytes N is the memory companion - it caps total heap allocation (collections, tuples, closures, and the string / bytes / bignum backing bytes those objects hold) at N bytes across the run, faulting the same way (exit 250, with the same sandbox default), so CPU and memory are both bounded. The byte count is a deliberately conservative over-approximation - an Arc-shared payload held by several objects is charged once per holder - since a security ceiling should fail early, never late. hanki test takes both --max-steps and --max-bytes too - they bound each test, and a test that exceeds a budget fails (reported directly, never shrunk into a counterexample like a logic failure is). This is the bytecode tier's fuel-sandboxable mode (§22); the AOT throughput tier omits it.

Where those flags bound a whole run from the CLI, with_budget(bytes, steps) BODY end bounds a nested scope from within the language: it carves a sub-quota from the parent's remaining step + byte budgets — a child can never exceed the parent, and its spend debits the parent — runs BODY under it, and evaluates to Result<T, sys.BudgetExceeded> (T is BODY's type): Ok(v) on completion, Err(Exceeded) the moment the sub-quota is spent. Unlike the whole-run ceiling (which faults the run, exit 250), a with_budget overrun is catchable — the host survives an over-budget child and recovers by matching the result — so it is the in-language primitive for running untrusted or unbounded nested work (an embedded interpreter, a user-supplied predicate) under a bounded, recoverable ceiling. It nests: an inner with_budget sub-quotas the outer one, and a normal throw inside the body still propagates through it (only budget exhaustion is intercepted). Bytecode tier only, like the flags it scopes — the AOT lowering rejects it (that tier has no resource metering).

• hanki scoreboard shows the package's compiler-verified Guarantees and measured Metrics - the un-gameable facts, before you publish. hanki scoreboard PATH prints a board of independent figures - deliberately never a single ranked score (a scalar invites Goodhart gaming). The Guarantees are facts the toolchain proves: Pure Hanki (no native @intrinsic in the package's own code), Crash-free (no crash! reachable from the public API - read off the Crash effect, which crash! charges and the effect discipline propagates to every public action that can reach it), the Effect bound and Throw surface a consumer inherits (the union of declared effect rows and throws types), and Docs complete (every public symbol carries a runnable example - the same check as hanki doc --check). The Metrics are measured numbers, labelled as such: the Purity breakout (% pure def · % @encapsulated · % actions, the @encapsulated share broken out rather than folded in), public-API size, module and line counts, test / property-test counts, and - with --coverage - a measured line-coverage % (which runs the package's tests under a recorder; opt-in because it executes code, bytecode-tier and line-only). "Public surface" is the non-_-prefixed names. --format=json emits one hanki-scoreboard-v1 envelope ({schema, entry, guarantees, metrics}). Because Guarantees are derived, a registry can recompute them from pinned source, so searching packages by a provable property ("a parser that provably never touches the network") is meaningful where a self-reported badge is not. (The dependency-mix facts are a planned extension; the closure is the leaf workspace until package dependencies exist.)
• hanki refresh re-syncs the compiler-managed files in a scaffolded project. The counterpart to hanki new: run from a project root (or pass its path) it rewrites exactly the managed set - HANKI.md, HANKI-CARD.md, skills/*, the .claude/skills/ adapters - to the current compiler's embedded copies and adds any newly-shipped skill, so a project's reference docs track the toolchain you build with. User-owned files (AGENTS.md, CLAUDE.md, main.hk, hanki.config.hk, source) are never touched. Idempotent (Already up to date when current); --dry-run lists what would change without writing.