Build a forum API with an agent

Before adding a handler

Start with the Forum’s organization map. Find handlers similar to the one you need, then follow their shared validation, access, and response helpers. Ask your agent to identify which existing definitions it can reuse and where the new behavior would live before it edits the program.

The map’s extension exercise compares a shared response with fields a caller can extend. Use the proposed feature to judge the interface. After editing, compare the same handlers again and choose the checks relevant to the change. The walkthrough below starts with compilation and access checks.

A calculation can be a public API

An identity-free calculation can use public_route with a handler taking its request directly: def calculate(input: Input) -> IO[Result]. It needs no dummy database parameter. The engine supplies Db, Principal, and no-payload Unit arguments from the checked signature; an anonymous handler cannot request a principal.

You can omit AccessSpec when verification establishes no storage effects across the supplied bindings and their reachable helpers. Unknown externals, indirect effect calls, or missing metadata leave this check blocked. Once the program uses storage, declare its policies and permissions as the forum example below does.

Decimal inputs and results

A Float64 API field accepts a quoted decimal such as "1.25" and returns the same wire format. The generated form accepts decimal text directly. Records, lists and union payloads use the same field schema, so you do not need a whole-dollar conversion adapter.

These are finite binary64 values with floating-point rounding. Signed zero survives JSON; malformed inputs, overflow, nonzero underflow to zero, and computed infinities or NaN produce errors. Use a decimal or integer-unit model when the calculation requires exact decimal arithmetic.

0. Clone and build the command-line tool

Java 17 or newer and sbt. The build writes one jar; the alias below is what the rest of this page calls yichus.

git clone https://github.com/snoble/yichus && cd yichus
sbt assembly
alias yichus='java -jar target/scala-3.8.2/yichus.jar'

1. Type-check what the agent wrote

yichus build compiles the file and every package it imports. A program that does not type-check stops here with the compiler's message, and nothing below runs on it.

yichus build demos/service/forum.bosatsu

Verbatim from docs/forum-demo/outputs/step1c-build.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

$ yichus build demos/service/forum.bosatsu
Parsing 1 file(s)...
Type-checking...
Success! Type-checked 31 package(s):

What it does not say. That the service does what was asked. Type-checking is the floor: the rules, the routes, and the runs are the next three steps.

2. Prove the access rules over every handler

yichus api verify checks the service’s declared access policies against the modeled database operations: owner-key discipline for owner-scoped tables and guard dominance for guarded tables. The first line summarizes the checks. Each property reports proven, violated, blocked, or warning, with its evidence and assumptions. A check can be blocked when the analysis cannot establish it.

yichus api verify demos/service/forum.bosatsu

Verbatim from docs/forum-demo/outputs/step1c-verify.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

$ yichus api verify demos/service/forum.bosatsu
proven False
compiles proven
access-spec-declared proven
    profiles: OwnerScoped
    threads: Guarded(can_see)
    posts: Guarded(can_see, can_edit)
    moderators: Public
access-coverage proven
...
access:posts proven
...
    Demo/Forum::post_reply db_write on "posts": dominated by can_see(Principal.user_id, row of threads), on the row it was applied to (key thread_id)
...
rmw-transactions violated
    Demo/Forum::grant_moderator reads then writes "moderators"; with multiple instances on one DB, run this handler in a transaction (or a single-writer queue) to avoid lost updates (topology undeclared or multi-instance: fix the handler or declare instances=1)
...
integrity violated
    race-free:moderators: 2 valid orderings over 'moderators' produce differing effect sequences (topology undeclared or multi-instance: fix the handler or declare instances=1)
    race-free:posts: 3 valid orderings over 'posts' produce differing effect sequences (topology undeclared or multi-instance: fix the handler or declare instances=1)

Reading the verdict. proven False here is two checks about deployment, not about the rules: a handler that reads a table and then writes it (rmw-transactions) can lose an update when two engine instances share one database, and the orderings check (integrity) counts the interleavings that would differ. The access checks above them are all proven. Declare the topology and the same run reads:

yichus api verify --instances 1 demos/service/forum.bosatsu

Verbatim from docs/forum-demo/outputs/step1c-verify-instances-1.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

$ yichus api verify --instances 1 demos/service/forum.bosatsu
proven True
compiles proven
...
    Demo/Forum::grant_moderator reads then writes "moderators"; with multiple instances on one DB, run this handler in a transaction (or a single-writer queue) to avoid lost updates (accepted: instances=1 declared; one instance runs each request's IO plan atomically)
...

What it does not say. That the guard is the right guard: the proof shows every write to posts sits under can_see applied to the caller, and the reader judges whether "any member who can see the thread may reply" is the rule that was asked for. Nothing here reads the guard's body.

3. Run one handler on seeded rows, and keep the record

yichus why evaluates one binding on inputs you give, in a fresh in-memory world seeded with the rows you give, then varies each input and reports what moved. --record writes the run with the sources it ran over to a file. The run below asks whether a stranger can read a members-only thread: carol is in no member list, the thread t1 admits bob.

ROWS='{"threads": {"t1": {"id": "t1", "title": "private planning", "author": "alice", "visibility": {"Members": {}}, "members": ["bob"], "reply_cap": 2}}, "posts": {"t1": [{"id": "p1", "thread_id": "t1", "author": "bob", "body": "first", "edited": false}]}, "moderators": {"roster": ["mona"]}}'
yichus why --binding Demo/Forum::read_thread \
  --inputs '{"p": {"user_id": "carol", "roles": []}, "req": {"thread_id": "t1"}}' \
  --rows "$ROWS" --seed 7 --variations 3 \
  --record read_thread-as-carol.json demos/service/forum.bosatsu

The replay script summarizes the JSON the command prints; the summary for this run, with the sentences the response carries:

Verbatim from docs/forum-demo/outputs/step2-why-read_thread.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

## read_thread as carol   (record: docs/forum-demo/records/read_thread-as-carol.json)
output: "Response(status: 403, body: \"{\"view\":\"forbidden\",\"rule\":\"members only\",\"message\":\"This thread is for its members only.\"}\")"
notReached: bool_literal, jarr, jarr_of_str, jbool, jint, jraw, not_found, posts_table, render_post, render_thread, render_visibility, respond
varied: parameter 'req' -> Response(status: 404, body: "{"view":"not_found","what":"thread"}")
...
narrative:
    This run evaluated the handler 'read_thread' (package Demo/Forum) with 'db' (the world's database), 'p' = Principal(user_id: "carol", roles: []) (provided) and 'req' = ReadThreadRequest("t1") (provided). It returned Response(status: 403, body: "{"view":"forbidden","rule":"members only","message":"This thread is for its members only."}").
...
    Proven for every input, by static dataflow (no run needed): 'db' may reach the result, so no run can rule its influence out; 'p' may reach the result, so no run can rule its influence out; 'req' may reach the result, so no run can rule its influence out.
...
    Observed on this run, not proven (bounded-observation (seed 7, one recorded handler run; 3 variations per aspect, each on a fresh world from the same seeded rows)): changing field 'user_id' of parameter 'p' across the seeded values never changed the result, which does not show independence; changing field 'roles' of parameter 'p' across the seeded values never changed the result, which does not show independence; changing parameter 'req' from ReadThreadRequest("t1") to ReadThreadRequest("moderators94") moved status from 403 to 404 (+1) and body from "{"view":"forbidden","rule":"members only","message":"This thread is for its members only."}" to "{"view":"not_found","what":"thread"}". Seeded and varied values are drawn from the seed, not from the domain: an integer may be negative or far outside any expected range. The run forced global values for 11 definitions: can_see, forbid, is_moderator, jobj, join_with, jstr, member_String, moderators_table, quote, roster_key, threads_table. Loading a function value does not establish that its body ran. Global values for 12 definitions this one can reach were not forced on this input: bool_literal, jarr, jarr_of_str, jbool, jint, jraw, not_found, posts_table, render_post, render_thread, render_visibility, respond (an absence on this input, not a fault; another input may force them).
...

Reading the run. The output is a 403 with the rule that refused it. notReached lists global values this input did not force. A function value can be loaded when a handler is registered without its body being invoked, so this set is not function-call coverage. The returned 403 is the observed refusal; the reference set alone does not establish which bodies ran. The sentences keep two kinds of fact apart: proven for every input comes from static dataflow and needs no run; observed on this run comes from a handful of seeded variations and is never a proof. "Never changed the result, which does not show independence" is the tool refusing to promote an observation.

The record. read_thread-as-carol.json now holds the request, the seeded rows, the response, and every source file's content. yichus why --replay read_thread-as-carol.json compiles those sources again, re-runs the request, and prints replay: identical or the keys that differ; the replay compares the new result with the saved result. Engine or dependency changes can produce a difference. This repository keeps the forum's ten records under docs/forum-demo/records/.

4. Open the record on the page

The WebMCP workbench runs the same engine in the browser. Under Why: evaluate one binding, see what moved, press Open record and choose the record file (this repository's copy of the run above: read_thread-as-carol.json, saved from the raw view). The page compiles the record's embedded sources, fills in the binding, re-runs the recorded request, and shows the same sentences under the output line. Below them, Proposed next lists the experiments the run's facts make discriminating, each a complete request; press Run on one and its output prints beside this run, never replacing it. Copy as yichus why prints the command-line invocation that reproduces the run on the CLI.

What it does not say. The page proposes experiments, never verdicts. Which of them to run, and what its result means for the rule you asked for, is the reader's.

Where to go next

• Reading the organization lenses: the pages that show what the agent built, in what shape, and how the parts are used.
• API MCP getting started: the five tools an agent calls for a typical API and what each result means.
• The forum walkthrough: the whole exercise, every step's prompt, and what the tools caught.