HomeAboutPostsTagsProjectsRSS
┌─
ARTICLE
─┐

└─
─┘

For a long time I talked to coding agents in Emacs through agent-shell . It worked well, except for one thing, and that one thing was the biggest problem: I could not type while the agent was writing its output. I would read the first lines of an answer, know what I wanted to say next, and then wait for the agent to finish before I could start. Every turn broke my train of thought.

So when I wrote an Emacs client for my own agent, the first requirement was an input area that is always available. My first version had two buffers. The conversation was a read-only buffer in one window. The place where I typed was a second buffer, with its own major mode, in a side window under it. I could type at any time — but the split cost me something small every few minutes. Closing a session meant closing twice, once per window. Getting back to the input meant finding out which window had focus, or typing a buffer name like *agent-input: work*.

So I moved the input area into the output buffer. It is now a few lines of ordinary text at the end of the conversation. This post explains how that works, and then how I made it stay on the bottom row of the window, down to the pixel. The first part took an afternoon. The second part took a day.

The figures are small models you can operate. Press the buttons: each one computes its answer the way Emacs does.

Part 1: an input area inside a read-only buffer

The output buffer must stay read-only: the agent writes there, and I must not change its words by accident. The input area must accept typing, at any time, even while the agent writes. This part shows how one buffer does both.

The whole session is one buffer, shown in one window. Read it top to bottom:

mode line… older output scrolls away upward …⏺ Read lisp/cordis-input.elThe draft starts where output ends,so one marker serves both.⏺ Bash make test42 passedmodel · in plan · ctx 12%>fix the flaky test first,then rerun it▌new output isinserted hereagent outputread-only text;grows, and moves upanchorinput areaconfiguration line,prompt and draft;stays on the last rows
The output fills the window from the top. Right after its last character is the anchor, and after the anchor, on the last rows of the window, is the input area.

The part after the anchor is the input area: a configuration line (model, strategy, effort, context use, queued messages), the prompt > , and the draft I am typing. It is plain buffer text. There is no widget and no overlay.

One position, two jobs

The client already kept a marker for “where does the next piece of output go” (cordis--insert-marker). The input area needs a marker for “where does the input area begin” (cordis--region-start). These are the same position, so I made them one marker. Two markers that must always be equal stop being equal the first time someone updates one and forgets the other.

So new output is inserted at the anchor, and everything after the anchor — configuration line, prompt, draft, cursor — moves forward as one piece.

Three text properties make the draft writable

The buffer is read-only; only the draft must accept typing. Emacs can do this with text properties alone, because of one rule: a character you type copies the text properties of the character before it, except the ones that character lists in rear-nonsticky.

The client sets three things:

propertyset oneffect
read-only, with front-stickythe output and the configuration linenothing can be typed into it, or in front of it
rear-nonsticky (read-only face cordis-prompt)the last character of the prompta typed character does not copy read-only or the prompt’s face, so the draft is writable and looks like a draft
keymap (the input keymap), not in the list abovethe promptevery typed character copies the input keymap: RET inserts a newline, C-RET sends, M-p/M-n walk history

Try it. Type into the draft, then let some output arrive:

read-only face (prompt) keymap (input map) rear-nonsticky stops here
Press a button. Each cell is one character of the buffer; the bars under it are its text properties.
Each cell is one character; the bars under it are its text properties. The red wall after the prompt is rear-nonsticky: read-only and the prompt’s face stop there, the keymap goes through.

The third row of the table is the one I did not expect to work. keymap is a text property that Emacs checks when it looks up a key. So the input keymap needs no minor mode, no overlay, no toggle. It arrives with the prompt, and each character I type passes it on to the next one.

This removes a whole category of state. There is no “input is active” flag to keep in step with focus, because there is nothing to activate. The draft is text in a read-only buffer, and the only thing that makes it writable is that the read-only property stops at the last character of the prompt.

Taking the keyboard back from special-mode

The output buffer’s major mode derives from special-mode. That mode is for buffers you read, not buffers you type in, so it binds printable keys to commands: q closes the window, SPC and DEL scroll, and 0–9 and - are prefix arguments. In the input area I could not type q — and, worse, I could not type a digit.

A text-property keymap is checked before the major mode’s map. That order is what lets one buffer have two keyboards. The fix is two forms in the input keymap:

(map-keymap (lambda (key _binding)
              (when (and (integerp key) (<= 32 key 126))
                (define-key map (vector key) #'self-insert-command)))
            special-mode-map)
(define-key map [remap self-insert-command] #'self-insert-command)

The first form is a sweep, not a list. It walks special-mode-map and takes back every printable key it binds. If a later special-mode binds a new key, the sweep takes that one back too — and the test walks the same map, so it notices.

The second form looks redundant. It is not. special-mode-map contains (remap keymap (self-insert-command . undefined)), and Emacs applies remaps after it finds a binding. With the sweep alone, every key finds self-insert-command, and then the remap turns it into undefined. Switch the two forms off and on:

point is in
press
    Lookup goes top to bottom and stops at the first map with a binding; then the remap pass runs. Try a in the input area with only the sweep on.

    In the output, above the anchor, nothing changed: SPC still scrolls and q still closes the window.

    Scrolling that nobody has to write

    The old client had a mechanism to keep the output scrolled to the bottom, and it had grown large: a cordis-follow window parameter, a window-scroll-functions observer, an initializer on window-buffer-change, a resume-following command, and a set-window-point after every write.

    It had a reason to exist. A fully read-only buffer has no natural home for the cursor, so the code could not tell “the user watches the bottom” from “the user scrolled up to read”. It guessed from the geometry and moved the window.

    With the input area in the buffer, that mechanism became a bug. The cursor now lives in the draft, and every write moved it. If I corrected a word in the middle of my draft and a line of output arrived, the cursor jumped to the end of the draft — 37 characters, in the case I measured.

    I deleted all of it, and nothing replaced it. The cursor is in the input area, and Emacs always keeps the cursor’s line visible. So new output appears above the input area, older text scrolls up and away, and the input area stays where it is. A terminal gets this effect from a scroll region; here it falls out of where the cursor is.

    Twelve tests went away with the mechanism. Two new tests replaced them, and both assert something that must not happen: arriving output must not move window-point, whether the cursor is in the draft or up in the output.

    Part 2: keeping the input area on the bottom row

    That is enough while the buffer is taller than the window. It fails at the start of a session, and it is not quite right later either. The two cases need different fixes.

    A short buffer: pad the top

    A terminal owns a screen of fixed height and reserves the bottom rows for the input (I compared how agents do it in How Coding Agents Draw Their Input Box ). The input’s position is fixed by construction.

    An Emacs window has no such thing. It shows a buffer from some start position downward. A short buffer is shown from its first line, so the input area sits right after the last line of text — in the middle of the window, with empty rows below it. Every new line of output pushed it down one row. In a fast stream it slid down the window until the text filled it.

    The fix makes Emacs look like the terminal, out of text: insert blank lines before the output, so the buffer is exactly as tall as the window.

    (max 0 (+ have (- height lines)))
    

    height is the window’s height in lines, lines the buffer’s height in display lines, and have the pad already there. As the output grows, the pad shrinks — measured 44 → 20 → 0. At 0 the text fills the window, normal scrolling takes over, and the client stops computing the pad. That also saves time: count-screen-lines walks the whole buffer, and a long session would pay for it on every line of output for nothing.

    Drag the slider, and turn the pad off to see the old behaviour:

    Hatched rows are the pad; amber rows are the input area (configuration line, then draft). Without the pad, the input area floats in the middle of the window until the output fills it.

    Two details matter later. The end of the pad is a marker, not a count: when the output is cleared, the marker falls back to point-min and the pad is zero by construction — nothing has to remember to reset it. And the pad is real newline characters with the output’s read-only properties, not a display trick. That matters for the pixels.

    A long buffer: pin the window start

    When the text is taller than the window, the bottom row still belongs to nobody. Emacs only promises that the cursor’s line is visible. The cursor is on the draft, the second line of the input area, so the configuration line above it may be cut off. The window start jumped between two positions one row apart: origin rows 64/66 alternating with 65/67, and the cursor at y 1354, then 1334.

    So the client sets the window start itself. The output gets h - K rows, where h is the window height and K the input area’s height. K is measured with count-screen-lines, not assumed to be 2, because a long draft wraps. It is capped at half the window, the same limit the terminal version uses.

    One detail cost me a few pixels of draft. The input area usually begins at the newline that ends the last line of output — and that newline belongs to the output’s display line. Counting h - K lines up from it starts one line too high, and pushes the draft below the window’s bottom edge.

    The last few pixels

    vertical-motion moves by whole lines, but the lines in this buffer do not all have the same height:

    • body text is 20px;
    • Markdown headings are 22px, because the heading face is :height 1.1;
    • a line with an emoji or a fallback glyph is 27px.

    In a 266-line session, 24 lines were not 20px. So whole lines almost never add up to the window height exactly: a gap of 0 to 19 pixels is left at the bottom, and its size depends on which lines happen to be on screen. I kept the tall headings. They are a big part of why this reads better than the terminal, and I would rather pay for them here than flatten the type. The terminal pays nothing, because every cell there is the same size.

    Emacs has one setting for a partial line, window-vscroll, and it does not hold here:

    • it works for one redisplay and is reset to 0 as soon as window-start changes (set 13, read back 0);
    • set from window-scroll-functions, it sees the old window start and corrects too much.

    What holds is a real character: one space at the end of the configuration line, with a display property of (space :height X). It is text, so redisplay has to lay it out; it cannot decide to ignore it. Add lines of different heights, then turn the spacer on:

    The bottom 200px of a window, drawn at 1:1. The window start can only move by whole lines, so a remainder is left under the draft. The spacer makes the configuration line exactly that much taller.

    Two facts about the spacer I had to measure, not reason out:

    1. (space :height N) ignores integers. 27 still gives a 20px line. The value must be a multiple of the base line height: 1.35 gives 27px on a 20px base.
    2. The order must be set it to zero, measure, fill once. If the old height stays in while I measure, the measurement includes it, the next pass drops a line, and the two corrections fight. Measured, that fight settled at a 10px gap with the spacer at its maximum.

    Why it still flickered

    After all that, it was almost right: now and then the input area jumped up or down by one line. Finding out why took longer than building the feature. There were three causes, unrelated to each other.

    1. The pad was recomputed on the wrong event. I recomputed the pad when output was written. But the input area changes height on its own — that is what an input area does. Write a five-line draft while the agent works, send it, and the draft is cleared: the buffer is four rows shorter, and nothing recomputes the pad until the next line of output. For that stretch the input area floats up.

    The fix is post-command-hook. It runs after each command and before redisplay, which is exactly the deadline. A timer with zero delay is not the same: it runs after the frame is drawn. My earlier timer-based attempt was one frame late every time, and one wrong frame is what a flicker is.

    keyC-RETcommanddraft cleared,region −4 rowspost-command-hookpad 61 → 65redisplayframetimer, delay 0one frame lateframe Nframe N+1pad set in the hookregion stays on the last rowpad set in a 0-delay timerone wrong frame: a flickerpad set only on output4-row gap until more output
    One turn of the command loop. The hook is the last chance to change the buffer before the frame is drawn. Measured: without the hook, a 4-row gap after sending; with it, the pad goes 61 → 65 and the gap is 0.

    2. The hook that did nothing. For a while the hook was installed and had no effect, with no error in sight. Two things stacked up:

    • Emacs silently removes a function from post-command-hook when it signals an error. The symptom is “installed, does nothing”, and *Messages* is empty.
    • The error was mine. The function’s docstring was in Chinese, and I had put an ASCII " inside a quoted phrase. The string ended there, the rest of the sentence became code, and that code failed with void-variable when the command finished. The syntax check passed, because the file was balanced and parsed. A stray quote in a docstring is legal code.

    And define-derived-mode does not run its body again for a buffer that is already in that mode. Reloading the file gave the hook to the next session, not to the one I was testing in. There is now a re-arm path, and it installs the hook too.

    3. Someone else’s global hook. The last flicker was not about geometry at all. beacon-mode flashes the cursor line whenever a window scrolls. This buffer scrolls once per line of output, so beacon flashed on every line. Beacon lives on the global window-scroll-functions hook, so the client now removes it from that hook in this buffer only. The cost: toggling beacon later has no effect here until the mode is entered again.

    One suspect was cleared, and it was the first thing both the agent and I guessed. scroll-preserve-screen-position is t in my configuration, and “keep the cursor’s screen row” sounds exactly like something that could oscillate. Turning it off locally gave the same frames, one for one. Not guilty.

    What it costs

    costdetail
    blank space at the top of a new sessionthe pad. The terminal version shows blank lines in the same place
    the draft moves when the configuration line changes widthctx 12% → ctx 9% shifts the draft a character or two; the terminal’s prompt line does the same
    the input area is redrawn on every status changethe configuration line is text, so it is rewritten, and the rewrite must put the anchor back, or the next output lands between the configuration line and the draft
    one buffer-local defencea third-party scroll hook is removed for this buffer
    auto-window-vscroll offthe last line is computed at 1360/67 ≈ 20.3px and loses about 3px — every time, instead of sometimes. Tall inline images in the output would want it back

    Traps, in one table

    trapwhat you seewhy
    rear-nonsticky must list every property that must not be copiedthe first key typed in the draft signals text-read-only, and the draft has the prompt’s facetyped characters copy text properties by default
    a macro that splices its body into a leta progress line that overwrote itself started to append insteadthe macro’s beg shadowed the body’s beg; no error anywhere, only the existing behaviour tests caught it
    an error inside post-command-hookthe hook is installed and does nothingEmacs removes a function from the hook when it signals
    an ASCII " inside a docstringthe syntax check passes; at runtime, void-variablethe string ends early and the rest is code
    define-derived-mode on a buffer already in that modereloaded code never reaches the live sessionthe mode body does not run again
    (space :height N) with an integerthe spacer seems to do nothingintegers are ignored; the value is a multiple of the base line height
    reading pos-visible-in-window-p while writing outputthe pin is skipped at random and the window start alternatesit answers about the frame before redisplay
    window-vscrollworks for one redisplay, then reads 0a new window-start resets it

    If you want this in your own client

    Without the war stories:

    1. One anchor. The place where output is inserted and the place where the input area begins are the same marker.
    2. Put the input keymap on the prompt as a text property, and use rear-nonsticky to choose what a typed character copies.
    3. Take the keyboard back from special-mode with a sweep over its map, plus a remap of self-insert-command back to itself.
    4. Pad before the output while it is shorter than the window. After that, set the window start yourself.
    5. Fill the last pixels with a real character that has a display height, not with window-vscroll.
    6. Recompute on post-command-hook, not on a timer: the input area changes height without any output.
    7. Never read window state while writing output. What you can read there describes the previous frame.

    If I could keep only one of these, it would be the keymap that travels with the prompt. It is why there is no input mode, no “active” flag and no second buffer. The input area is not a widget that the output buffer hosts. It is text at the end of the buffer that happens to be writable.

    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    Every coding agent I use handles a long conversation the same way. It lets the context grow until it gets close to the window, sends the whole thing back to the model with “summarize this”, and carries on from the summary. Claude Code calls it auto-compact. Codex does it. My own agent, a small harness written in Rust, did it too.

    For a while now my agent has worked another way. I think it is the better default, and I have not seen anyone else talk about it. I call it a context fold.

    The short version: don’t wait for the window to fill. Ask the model, again and again, one small question: is anything behind you finished? It is a hard question to answer about the future and an easy one to answer about the past.

    What is the model actually reading?

    I measured my own sessions: 221 of them, 853 user turns, 12,268 tool calls. For every request I split the context into three parts:

    • the work in progress,
    • the conclusions of finished work,
    • the steps of finished work: the tool calls, their outputs, the dead ends.

    With no processing at all, the third part is two thirds of what the model reads. The conclusions of that same finished work are about 1%.

    That is not mostly a cost problem. Prompt caching makes old tokens cheap. It is an attention problem. On every turn, the model reads through a long record of how the login test got fixed, only to find out what to do about the build.

    Compression waits for the wrong signal

    Compaction fires on the water level. That has three consequences:

    1. The timing has nothing to do with the content. It fires in the middle of a task, when the context is most useful. The trigger is “the window is full”, not “this part is done”.
    2. The replacement is a paraphrase, and the original is gone. The harness may keep a backup file, but the model cannot read it back. Whatever the summary left out does not exist any more.
    3. It costs a model call. The whole context goes in and a summary comes out, and output tokens are the most expensive kind and cannot be cached.

    Here is the same session under both rules. On the left, compaction. On the right, folding.

    Rows are messages. you ▸ is a user turn, indented rows are tool calls, ◆ is the model’s closing message for a piece of work. The fold card thresholds are shrunk to fit the demo. In the real harness the host asks after about 20 tool calls, not after every turn.

    Look at turn 4, “ok, turn it off”. It is short and it reads like a new instruction, but it continues the build question. The model sees that and folds nothing. The last unit is still open, so it stays word for word.

    Boundaries are easy in hindsight

    The obvious fix is to cut the conversation into tasks and drop the finished ones. The hard part is where a task starts.

    I tried a lexical rule first and checked its output by hand:

    The rule saysIt is right
    “a new task starts here”20–33% of the time
    “this continues the last one”97.4% of the time

    Half of all user messages are 60 characters or less. “all of them need to be improved” and “you decide, it’s fine, go ahead” look like new instructions. They are not. And work gets tangled: a new task often starts as a side remark and turns into a task three turns later. Looking forward, you cannot tell.

    Looking back, you can. When a piece of work is done, the model has just written its conclusion: fixed, the race was in session setup. From that end, the start is plain to see. It is like parentheses. When you open one, you do not know how deep you will go. When you close one, you always know which one you are closing.

    So the host does not try to find the boundaries. It does what it is good at, which is counting, and filtering out the 97% of turns that are plainly continuations. The model does the one thing only it can do: it judges the content.

    How a fold works

    The card. When enough work has built up since the last fold (about 20 tool calls, or about 100k tokens), the host attaches a short card to the user’s next message. The card lists the turns since the last fold, their sizes and the paths they touched, and each user message word for word. Then it asks one question. The host numbers the turns, so the model picks from a printed menu and never has to count. “Ignore this” is a valid answer. When nothing is closed, the card cost about 250 tokens and that is all.

    The answer. The model calls fold_unit(from, to). The host checks only that the call is legal: the turns exist, the range is not reversed, there is no earlier fold inside it (folds do not nest, because each level loses a little more), and the turn in progress is not part of it. The unit the model is working in is never foldable.

    The splice. After the turn ends, the host first writes the original messages to an archive file with a sha256, and only then replaces the range with a single result message. That order matters: a result must never point at an archive that does not exist.

    The result. The host builds the result itself, with zero model calls, from three parts:

    • a mechanical index: tool calls counted by name, the paths they touched, the number of shell commands. The host counts these, so they cannot be wrong;
    • every user turn in the range, word for word. The user’s decisions are the one thing no tool can find again;
    • the model’s own closing message for that unit, which it already wrote.
    A mock-up. The card’s wording is shortened and its turn texts and sizes are made up. The outcome is from a real resumed session: turns 1–4 offered, 1–2 chosen, 337 messages down to 69. The result carried 146 tool calls (116 of them shell commands), 7 paths, both user turns and a 1.7 KB closing message.

    Reading it back. The archive is an ordinary file. If the result turns out not to be enough, the model reads the file with read or grep, the tools it already has. There is no special “unfold” tool and no undo command. An undo would push the wrong way: if a fold can always be undone, nobody has to make the result good enough to stand on its own.

    Why not just trim old tool output?

    Some agents cut old tool results on every request. I decided against it, for one rule:

    Anything you drop must have an archive, an address and an index. If it does not, don’t drop it.

    Trimming has none of the three. It even removes the record that a file was ever read, so the model has to rebuild its state from nothing. I ran a small A/B test: a two-turn task, three runs per arm, with trimming the only difference. Both arms got the right answer. But in turn 2 the trimming arm re-ran every tool call from turn 1: 4, 4 and 4 calls against 0, 1 and 1.

    What it buys

    On that resumed session, replaying its real fold points against the same session without folds: the median request was 0.2× the size, about a fifth. By the end of the session it was a sixth. That is one session. The ratio is solid; I would not generalize from it.

    Prompt caching is what worried me. A fold edits the middle of the conversation, so everything after the fold point misses the cache once. I simulated the options. Fold as soon as a unit closes: 217 folds, a median of 17k tokens rewritten each. Wait for pressure and fold then: about 30 folds, a median of 200k each. The totals came out within 21% of each other. When you fold does not change how much you rewrite. It only changes whether you pay in many small pieces or a few big ones.

    Compaction is still there, as the emergency path:

    CompactionFold
    Fires whenthe window hits a trigger linea unit of work closes
    Who decidesthe hostthe model, with one tool call
    Replacementa summary, written by the modela result, put together by the host
    Model callsone, over the whole contextzero
    The originalcannot be read by the modelon disk, with an address
    Runsin an emergencyall the time

    Strategies: the context as a call stack

    A fold draws the parentheses after the fact. Sometimes you know in advance. “Go find out why CI is flaky” is a detour, and you know before you start that it will open and close.

    For that, my agent has strategies. A strategy is a mode: a set of standing instructions, an explicit way in and out, and a label on the status line so the user always knows they are in one. Mechanically, it is a stack frame:

    • Enter (strategy_request, or the user types /strategy). The host appends one message at the tail of the conversation, with the rules of the mode. It does not change the system prompt or the tool list. Those always stay the same. So the whole prefix is byte for byte what it was, and the next request hits the cache.
    • Inside, the model works in the same context. It sees everything the main loop saw, so nothing needs to be explained again.
    • strategy_report is the return value. The model rewrites it as the work goes along.
    • Exit (strategy_yield, or the user types /back). The whole branch folds away. The main conversation keeps exactly one thing: the latest report.

    That is a function call. Push a frame that shares the caller’s environment, do the work, return a value, pop. The general-purpose one is errand, whose rules are three lines: do only this task, keep the report current, yield when you are done. The others follow the same shape: triage works through a queue with the user deciding each item, intent is a read-only mode for agreeing on what to build, and counsel hands a hard problem to a stronger model.

    The return value is written, not scraped

    This is the point I most want to get across. You cannot get the result of a piece of work out of its transcript afterwards.

    The obvious way to build a strategy is: when the mode ends, read the branch and summarize it. That is compaction again, in a smaller box, and it is lossy for the same reason. The transcript records what happened, not what mattered. Take forty tool calls. Which grep answered the question? Which idea was dropped, and why? Of three edits, which one is the fix and which two were experiments? The model knew each of these at the moment it happened: when the log line matched, when the test went green. Afterwards, that knowledge is spread over forty outputs that all look equally important, and whoever writes the summary has to guess it back. That is true even for the same model reading its own transcript. It is reconstructing, not remembering.

    So the result is written as the work goes along:

    • strategy_report is a slot, not a log. Each call replaces the previous one, so the report always holds the current state of the work, not its history. The model calls it when it learns something: “3 failures, all EADDRINUSE” at the moment it sees the log, “tests share port 8080; fix: bind :0” at the moment the test passes.
    • strategy_yield is an explicit end. The model says the work is done and gives a reason. The host then takes the last report exactly as it is. Nothing is inferred on the way out, and there is no extra model call to write a summary.

    A side effect: if the user leaves in the middle with /back, the report is still current. It holds everything learned up to that point, because it was never waiting for the end.

    It is the same principle as the fold. A fold result is made of counts and the user’s own words, plus the closing message the model wrote when it finished. Neither mechanism summarizes after the fact. The only accurate record of what mattered is the one written at the moment it mattered.

    Subagents: a tool that thinks

    A strategy is a call on the same machine. A subagent is a call to another process. A fresh child sees only the brief it is given. It runs in the background, does its own searching, and hands back a receipt: the conclusion, not the search. From the main loop’s side it is just a tool that happens to think. A goal goes in, an answer comes out, and every file it read stays in its own transcript.

    The two differ in who is in the loop. Inside an errand, the user can still talk to the model. A subagent runs alone and comes back. And because a fresh child never saw my guess, it cannot hand my guess back to me. That makes it the cheap way to get a second opinion.

    Left: the one conversation the user sees. Middle: an errand pushed on top of it. Its prefix is the main loop’s, so entering costs one message, not a rebuilt cache. Watch its report box: it is rewritten while the work happens, and on yield that box, not a summary of the branch, is what goes back. Right: a subagent that starts from its brief alone and runs while the main loop keeps working.

    I measured whether delegating saves money. In my sessions it does not: the main loop already runs on a cheap model most of the time. What it buys is parallel work and room in the context window.

    One shape, three times

    In Lisp, once a form has been evaluated, what remains is its value. That is the picture I keep coming back to.

    The last form is still open, so there is nothing to fold yet. The closing parenthesis is the boundary, and you only get to see it once it is there.
    • A fold draws the parentheses after the fact, once the model can see where the work closed.
    • A strategy opens them on purpose, when you know a detour is a detour.
    • A subagent evaluates the form somewhere else and sends back the value.

    Compaction is what you do when you run out of memory. Folding is what you do when a function returns. A conversation where finished work has been replaced by its value is shorter, cheaper, and, which is the part I care about most, easier for the model to pay attention to.

    What I don’t know yet

    • How often the next turn needs something that was folded. This is the biggest unknown. Two numbers will tell: how often the model reads an archive back, and how often it re-runs a tool it already ran before the fold. A zero on the first is good news: it means the result stood on its own. I have the counters; I do not have enough folds yet to read them.
    • Whether the model folds too early. It could fold a unit the user is not done with. The damage is limited, since the user’s words are in the result and the original is in a file, but I have not measured how often it happens.
    • The boundary numbers. The 20–33% and 97.4% come from one reader, me, checking once. I trust the direction more than the digits.
    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    I maintain a small coding agent written in Rust. Its input area is home-grown: a bottom region fenced off with a terminal scroll margin, a half-cooked termios mode, and a line editor I wrote myself. It works, but it does not look or feel as good as the agents I use every day. Before I rewrite it, I wanted to know what the others do.

    I had one hard constraint: no full-screen TUI. The conversation must go into the terminal’s own scrollback, so that I can scroll up, search with the terminal’s find, and select text with the mouse as usual. Only the bottom part of the screen, the prompt and a status line, should be “live”.

    This post is what I found.

    The two ways to draw an interactive terminal app

    A terminal has two screen buffers. The main screen is where your shell lives; lines that scroll off the top go into scrollback. The alternate screen (ESC[?1049h) is what vim and htop use: a fixed grid with no scrollback, restored to the previous content on exit.

    An agent CLI has to pick one:

    1. Alternate screen. The app owns every cell. Redraws are easy and flicker-free, but scrolling, find, and selection are gone and have to be reimplemented inside the app.
    2. Main screen. Finished output is printed once and left to the terminal. The app redraws only a small region at the bottom. Scrollback, find, and selection keep working, but every redraw has to be careful, or the screen flickers and history gets corrupted.

    Peter Steinberger’s post The Signature Flicker describes this trade-off well, and it is the best single source I found. Mario Zechner’s write-up on building pi goes deeper into option 2.

    Who does what

    AgentRendererScreenScrollback kept?
    Claude CodeReact, first on Ink, then a custom differential renderermainyes
    Gemini CLIInkmain (alt-screen tried, rolled back)yes
    Command CodeInk + React (closed source)mainyes
    Codex CLIRust: ratatui + crosstermmain, with a scroll regionyes
    piown library, pi-tuimainyes
    opencodeOpenTUI (Zig core, TypeScript/Solid)alternateno
    Ampown renderer, replaced Inkalternateno

    Some notes on the rows:

    • Claude Code had the famous flicker, caused by Ink’s full redraws. Anthropic rewrote the renderer and kept React as the component model. The fix shipped in 2.0.72. Their stated reason for staying on the main screen: an app that draws its own selection and scrolling “would not feel like your browser”.
    • Gemini CLI announced an alt-screen TUI and rolled it back within a week. Users disliked having to press Ctrl-S before they could select text.
    • Command Code is not open source. Its npm package is bundled and obfuscated, but its changelog shows that it runs on Ink and pins ink to 6.6.0 to fix Shift+Enter in the VS Code terminal.
    • Amp moved to alt mode to kill flicker. Now the terminal’s find only matches text that is on the screen.
    • opencode built OpenTUI , which diffs individual cells and never sends an erase sequence. It is very well engineered, but it has known problems in older macOS Terminal and GNOME Terminal.

    The pattern: the agents that most care about feeling like a terminal stayed on the main screen. The ones that went full-screen got smoother redraws and paid for them with scrolling and selection.

    Three ways to stay on the main screen

    Among the main-screen agents, I found three designs.

    Ink-style React rendering. A component tree is re-rendered into a string, and the string is repainted over the previous frame. It is easy to write. The flicker comes from repainting too much, too often.

    Line-level differential rendering (pi-tui, Claude Code’s new renderer). The renderer keeps the lines it drew last time, compares them with the new frame, and rewrites only the lines that changed. It wraps each frame in synchronized output (DEC mode 2026) so the terminal shows the frame all at once. Limits: the cursor cannot reach lines that have already scrolled into history. So when something above the viewport changes, for example a Markdown block that reflows, the renderer has to clear and redraw everything. Clearing lines also cancels any mouse selection that is in progress.

    Scroll region plus insert-above (Codex CLI). Codex keeps its composer, status line, and popups in a ratatui viewport at the bottom. When a history cell is finished, it queues the rendered lines and insert_history pushes them above the viewport. It does this by setting a scroll region (DECSTBM, ESC[top;bottom r) and scrolling it, so the lines flow into real scrollback. The live area never touches history. Its issue tracker lists the costs:

    • In Zellij, a partial scroll region combined with clear-to-end-of-line can be read as an in-place wipe, and history lines are lost.
    • In Windows Terminal (ConPTY), lines scrolled out of a partial region often do not reach scrollback.
    • Terminals without mode 2026 (Tabby, Wave) show the cursor jumping between the status line and the composer.
    • Resize is the hard one. Committed scrollback cannot be reflowed by the app, so Codex re-renders the transcript from memory after a resize. Depending on the terminal, that means a flash, a jump to the top, or duplicated lines. Codex also has a full-screen pager (Ctrl+T) as an escape hatch.

    Steinberger also notes that Codex has been moving toward an alt-screen TUI. Even the Rust team that got this design to work was tempted to give it up.

    The Rust toolbox

    My agent is in Rust, so this is the part that decides what I build. The candidates for an inline, multi-line input area:

    LibraryMulti-line editingPrint above the promptNotes
    ratatui Viewport::Inlinevia a widgetTerminal::insert_beforethe officially supported form of Codex’s design
    tui-textarea yes, 2-D cursor, undohost’s joban editor widget for ratatui
    reedline yesExternalPrinterNushell’s line editor, designed for a shell prompt
    rustylineweak (continuation lines)noreadline clone
    termwiz LineEditorsingle-lineno
    crosstermbuild it yourselfbuild it yourselfthe primitives everything above uses

    I used a fork of reedline before I wrote my own editor. It is good at being a shell prompt. A pinned composer with a status line and a completion popup is not what it was designed for.

    What I take from this

    • Staying on the main screen is the right call for an agent that mostly prints text. Claude Code and Gemini tested the alternative in public, and both came back.
    • The editor and the renderer are separate problems. Most of what “feels better” in these agents (multi-line editing, paste, completion popups) is the editor. Most of what “looks broken” (flicker, lost history, resize artifacts) is the renderer. I can swap one without the other.
    • Synchronized output (mode 2026) is table stakes. Every serious renderer uses it.
    • Resize has no clean answer on the main screen. Nobody I surveyed has solved it. Everyone either replays the transcript or accepts some artifacts. I should decide which one I want before I start, not discover it later.

    For my own agent I see two paths. The small one: keep my scroll-region input area and replace only the editing core with tui-textarea. The large one: move to a ratatui inline viewport, as Codex does, and draw the composer, the status line, and the popups as widgets. Codex’s insert_history.rs and textarea.rs are Apache-2.0 and worth reading either way.

    A note on method: I collected this survey with an AI agent doing web searches. I checked the main claims against Steinberger’s post and the linked sources. I did not re-verify every issue in each project’s tracker, so treat the specific bug descriptions as pointers, not as a changelog.

    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    I wanted to know how much of Bend 2 I could actually put to work inside an ordinary TypeScript application, so I built a small demo that works out a bill from recorded usage. The billing decision lives in Bend, where a law that covers every input takes the place of a test suite that covers the cases I happened to think of. Everything else is plain TypeScript: the UI, HTTP, storage, and the npm packages around them.

    What got me to try it was this idea:

    The human says what “correct” means, an agent writes the code and the proofs, and the checker decides. Bend is the first tool I have seen that makes this division of labour work in everyday engineering.

    人负责说清楚"什么是对的",agent 写代码和证明,检查器负责判定。Bend 是我见过第一个能让这种分工在日常工程里实际跑起来的工具。

    This post is what that cost and what it gave back, roughly in the order I ran into it.

    Draw the line at IO

    I expected to split the code by importance: critical logic in Bend, the rest in TypeScript. The line that actually worked was IO. Anything pure can go in the proved core: data structures, algorithms, state machines, any computation whose answer has to be right. TypeScript keeps whatever touches the outside world: HTTP, files, the clock, the UI, and the npm packages that wrap them. The two meet in memory. The host calls the core as an ordinary function, through types generated from the Bend source.

    Billing was a good first candidate because of its shape, not its importance. It is a pure decision that must be right for every input, and its rules can be written down as laws. Permissions, quotas, allocation, scheduling, merging and protocol state machines have the same shape.

    A TypeScript type can say that a bill is a number. It can’t say that the bill is the sum of each unit’s price. Here is that statement as a Bend law, from my graduated-pricing core:

    law charge_exact:
      for +plan: C.Plan
      for n: Nat
      {C.charge(plan, n) == C.per_unit(n, plan) : Nat}
    

    charge walks the pricing tiers, per_unit prices one unit at a time, and the law says they agree for every plan and every usage. The proof is what makes “every” literally true.

    Once the first function is in, the next one is cheap. The first move pays for the bridge, the type generation and the test gate; after that, each pure function you move costs little, and the rest of the app barely notices. Over time the core grows and TypeScript thins into a shell around IO.

    What a proof gives that a test doesn’t

    It covers every input, not the ones I thought of. Bugs in decision logic tend to live in combinations nobody wrote a test for: a wildcard in an odd position, an empty list, a boundary value, a requester with no roles. I planted the same plausible bugs in a well-tested TypeScript function and in a proved core. The tests missed some of them. The proofs caught every one that the laws spoke about. The bugs the tests missed were the expensive kind.

    It forces the specification questions before any code exists. Writing a law makes you decide things a TypeScript implementation decides by accident:

    • Does a window that ends at 12:00 touch one that starts at 12:00?
    • Is a requester with no roles covered by a rule for “any role”?
    • What does a plan charge past its last tier?

    Without a law, the answer is whatever the code happens to do, and nobody knows a choice was made.

    It gives reviewers something they can actually read. A reviewer can read a dozen short laws and know what the core guarantees, without reading the code or the proofs, because the checker vouches that the code meets them. I didn’t expect to care about this as much as I do.

    Most of the value came before the proof

    The steps leading up to the proof caught most of the problems:

    • Reading the existing code to list what it had to guarantee turned up bugs in it: edge cases it got wrong, inputs it quietly mishandled.
    • Drafting the laws surfaced decisions nobody had made.
    • Falsifying the laws on concrete inputs exposed a wrong specification in under a second, before any proof existed. The checker can evaluate code on literals, so instantiating a candidate law a few thousand times gives you a property test with the checker as the runner.

    The proof comes last, and it is the cheap part. It turns “we checked a lot of cases” into “it holds for all of them”, and it keeps holding when the code changes.

    Designing for the proof made the code better

    How the code is shaped decides how hard the proofs are, so before writing anything I looked for the shape with the shortest induction. Again and again, that was also the better program:

    • A step the proof doesn’t need is often a step the program doesn’t need. Rewriting an algorithm so its correctness argument is a single induction can remove a whole phase, such as a sort.
    • Make invalid inputs impossible to write. If a bad value can’t be expressed, the laws need no precondition, the core needs no validation, and the proofs need no case analysis. TypeScript validates once at the boundary, where the error message can still say what was wrong.

    Sketching the proof is part of the design, not paperwork afterwards. One of my laws was satisfied by a version of the code that did nothing at all. The law was true and useless, and only sketching the proof showed it.

    Where a proof can still mislead you

    A proof is exactly as strong as what it states and what the checker enforces. Four gaps I ran into:

    • Proofs protect only what the laws say. A law written in terms of a helper says nothing about bugs in that helper. If “a matching deny means no” is stated with the core’s own matches, a broken matches leaves the law true. Laws about the helper itself close the gap. Choosing the laws is the real design work.
    • Proofs can’t see run time. They say nothing about stack depth, time or memory. A proved function can still overflow the stack on realistic numbers, and small literal test cases won’t show it. Test the core at real scale.
    • The host isn’t proved. The bridge’s conversions, validation, IO and configuration are ordinary TypeScript and need ordinary tests. Keep that layer thin and check its conversions against a trusted reference.
    • An unsafe definition can prove anything. A def that skips the termination check can “prove” a false equation, and the checker still prints “All terms check”, with a warning next to it. The gate has to reject that warning, not just look for the success line.

    And a proof that checks quickly may not be saying much. Three habits kept mine honest:

    1. Give every law a mutant. Change one line of the core so the law becomes false, and require the proof to fail inside its own lemmas. Make sure the mutated core still compiles; a mutant that doesn’t compile is caught for the wrong reason.
    2. Check that the falsifier can fail. Plant a bug and require a counterexample. Build test inputs around the law’s hypotheses: uniformly random inputs rarely satisfy them, so the falsifier finds nothing even when the law is false.
    3. Recognise equivalent mutants. A change that computes the same function, such as a < b ? a : b versus a <= b ? a : b, survives every law, and it should. Compare the two functions before calling it a gap.

    The cost is tokens, not people

    With one agent working sequentially, a proved core took several times longer than the same function with example tests. Most of that time went into deciding what the laws should say and how to shape the data, not into the proofs. Proofs usually checked on the first or second try: the checker answers in well under a second, and each error names the next goal.

    That cost falls on agents, and it parallelises. Several agents can attack the same law with different strategies, such as which argument to induct on or which lemma to state, and the first proof that checks wins. Since the checker is the judge, nobody has to trust or review an agent’s proof.

    The one cost that doesn’t parallelise is the human one: deciding what “correct” means. So keep laws short and readable enough that a person can approve a dozen in a few minutes. As more code moves into cores, reviewing laws becomes the main human job.

    The ecosystem is young

    Bend’s library ecosystem is small, but that is a matter of time rather than a limit on what belongs in Bend. I expect those libraries to be written by agents, and to come with proofs. A proved library has a property ordinary packages don’t: its theorems hold for every input, so it doesn’t break when used somewhere new. Proved facts also accumulate. A lemma about ordering, proved once for one project, gets reused unchanged by the next. One of my projects pulls in bend-mathlib as a submodule, and the few facts it lacks live in the project that needs them. Each proof makes the next one cheaper.

    For now, expect to work around a few things:

    • There is no official library output. I wrote bend-emit ( https://github.com/nohzafk/bend-emit ) to build a typed ES module from a core.
    • Editor support lags behind the compiler.
    • The JavaScript runtime is single-threaded and uses BigInt for numbers, and some standard-library functions that are easy to prove things about are slow at run time. Test at real scale.
    • The language’s rules are still being relaxed from release to release.

    Try it

    The idea held up. The human says what “correct” means, agents write the code and search for proofs in parallel, and the checker decides. With the boundary drawn at IO, formal verification stops being an academic exercise and becomes part of everyday engineering.

    I’ve packaged the method as an agent skill, bend-ldd ( https://github.com/nohzafk/bend-ldd ). It covers where a proved core belongs in an application, how to find the laws, and which tool to reach for when a proof won’t check.

    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    Bend 2 is a new programming language. It looks like Python, behaves more like Haskell, and tries to combine three things that rarely go together: proofs checked at compile time, C-like speed, and parallelism across CPU threads and GPUs from one source. Its guide is candid about the goal: to give people “an ambiguity-free language to communicate their intents to AIs”, with a compiler that checks the result mechanically.

    While learning it I wrote a short book, Bend 2, from zero ( https://nohzafk.github.io/bend2-from-zero/ ), where every claim comes with code you can run. Early on I wrote down a sentence I didn’t yet understand:

    Affinity is the first key to understanding everything in Bend.

    That is the kind of line that sounds deep and means nothing, so I tested it. I installed Bend 2.0.5, wrote small programs to see what the rule actually enforces, and then reread the language through it.

    The line held up. Bend advertises three things:

    • no garbage collector
    • parallelism without locks
    • proofs that cost nothing at runtime

    They look like three separate pieces of engineering. They turned out to be three consequences of one rule about who owns a value. This post is about that rule, what it costs, and where it parts ways with Rust, which is where most programmers have met the word “affine” before.

    Where the word comes from

    “Affine” isn’t Bend’s word. It comes from logic, from the question of what you may do with an assumption once you have it.

    A proof can treat an assumption (a variable) in three ways, known as the structural rules:

    RuleMeaning
    weakeningyou may drop an assumption without using it
    contractionyou may duplicate an assumption and use it twice
    exchangeyou may reorder assumptions

    Ordinary languages allow all three, which is why nobody thinks about them. In 1987 Girard removed weakening and contraction and got linear logic, where every assumption is used exactly once. Systems that drop some of these rules are called substructural type systems; the standard reference is David Walker’s chapter of that name in Advanced Topics in Types and Programming Languages (MIT Press, 2005).

    Putting rules back one at a time gives a family, and each member has a name:

    exactly once   linear
    at most once   affine       ← Bend is here, and so is Rust
    at least once  relevant
    any number     unrestricted ordinary languages
    

    Affine is linear plus weakening, nothing more. So Bend’s default fits in one sentence:

    A value may be used at most once.

    “At most” is not a loose way of saying “exactly”. It is the whole difference between affine and linear, and it can be tested.

    The rule counts paths, not occurrences

    This is the program that made it click for me. x appears twice in the source:

    import Base
    
    def describe(c: Bool, x: U32) -> U32:
      match c:
        case True{}:
          (x + 1 : U32)
        case False{}:
          (x + 2 : U32)
    
    def main() -> U32:
      describe(True{}, 10)
    
    11
    

    It compiles, because the checker counts uses per execution path, not per occurrence in the text. Any run takes one branch, so on every path x is used once.

    Two uses on the same path are refused, with a refreshingly direct message:

    import Base
    
    def main() -> U32:
      x = {3 : U32}
      (x + x : U32)
    
    Error:
    - expected : x
    - observed : x (consumed more than once)
    

    And the part people get wrong: not using a value is fine.

    def main() -> U32:
      x = {3 : U32}   # never used
      7
    
    7
    

    In a linear language this would be an error. Weakening is what makes an unused value legal, and, as we’ll see, it is also what makes destroying a value free.

    Two annotations: quantity on the variable, kind on the type

    Two different annotations are involved, and mixing them up cost me three failed experiments. One goes on the variable, the other on the type.

    Quantity goes on the variable:

    -x     erased      visible to the checker, deleted by the compiler
    x      affine      the default, at most once
    +x     reusable    may be used many times, at the cost of a reference count
    

    Kind goes on the type declaration:

    Type = Kind(&1)    at most once  — things with identity
    Data = Kind(&2)    copyable      — things without
    

    + is the escape hatch. It isn’t free, since +x makes the value reference-counted, and it isn’t always available: it requires the type to be Data. You can only copy what can be copied. Ask for it on a Type:

    def main() -> U32:
      +a = [0 : U32*4n]
      (a[0] + a[1] : U32)
    
    Error:
    - expected : Data
    - observed : Type
    

    Array is a Type, so it can never be +. List is Data, and the same kind of program passes:

    def main() -> Nat:
      +xs = {[1, 2, 3] : +List<U32>}
      Nat.add(List.length(&2, U32, xs), List.length(&2, U32, xs))
    
    6n
    

    (The &2 passes the quantity to List.length explicitly. Bend puts the count in the type rather than inferring it.)

    Which types are Type, then? In the Base library, 13 types are Data and only 3 are Type:

    Array      a block of mutable memory
    IO.OP      an I/O operation
    App        an application / window state
    

    All three have an identity. Copying a block of mutable memory would break the in-place update that makes arrays usable in a pure language. Copying an I/O handle would counterfeit a resource. Copying an application state would fork a window. Copying a List<U32> just copies a structure, and the two copies can’t interfere with each other. That is the entire reason +List<U32> is legal and +Array<U32> isn’t.

    What an array read returns

    The in-place guarantee is where affinity stops being abstract and starts shaping syntax. Reading an array consumes it, so a read can’t return just the element; the array would be gone. It returns both:

    def main() -> Array<U32> & U32:
      a = [0 : U32*8n]
      a[5] <- 42       # an in-place rewrite, not a copy
      a[5]             # returns the array AND the element
    
    ([0, 0, 0, 0, 0, 42, 0, 0], 42)
    

    You get the array back, with the write in it, and the element beside it.

    Array<U32> & U32 is sugar for a Sigma, a dependent pair. Bend only lets you open one where it was handed to you, as a parameter or a field, never at a local binding. So either give the code its own def, or use the two projections Base already provides:

    def main() -> U32:
      a = [0 : U32*8n]
      a[5] <- 42
      b = Pair.fst(Array<U32>, U32, a[5])   # the array half, write intact
      Pair.snd(Array<U32>, U32, b[5])       # the element half
    
    42
    

    Pair.fst and Pair.snd are one-line defs whose parameter is a pair, which is exactly the shape the rule asks for. The general pattern: whenever you read from a Type, the thing you read from comes back alongside the value, and a function parameter is where you take the pair apart.

    Three selling points, one rule

    The guide covers speed, parallelism and proofs in separate chapters, but each follows from “one value, one owner”, and the guide says so in passing.

    No garbage collector

    From the guide:

    There is no garbage collector. Since values are affine, a match frees the node it opens on the spot, and only + values carry a reference count.

    With a single owner, opening a node with match can free it immediately, because nobody else can be holding it. And because the logic is affine rather than linear, a value that is never used can simply be dropped. This also explains a rule that looks like style: in Bend you destructure with match rather than reaching for fields. That isn’t an idiom. It is the language’s memory management.

    Parallelism you don’t have to justify

    A parallel call is an ordinary assignment: two calls on the right, two names on the left. Here it is doing real work:

    import Base
    
    def pow2(+n: Nat) -> U32:
      match n:
        case 0n:
          1
        case 1n+p:
          a b = pow2(p) pow2(p)
          (a + b : U32)
    
    def main() -> IO(Unit):
      do IO<Unit>:
        IO.print(U32.show(pow2(10n)))
    
    1024
    

    The two calls run as two tasks and are joined by the assignment. Both read p, the predecessor bound by case 1n+p, which is only legal because +n makes it reusable. Remove the + and the line is refused with the error from earlier: expected : p, observed : p (consumed more than once).

    The guide describes the contract like this:

    A parallel call promises the compiler two things: 1. The calls are independent. 2. They run in roughly the same time.

    Since Bend is pure and affine, the first point always holds. The second is yours to keep.

    This split is my favourite thing in the language. You never assert or prove that the two calls don’t interfere. The ownership rule already guarantees it: a second reference to a value can’t be written, so there is nothing to alias and nothing to race. What’s left for you is load balancing, which really does need a human.

    Put the other way round: in Bend you cannot write the racy program. For both sides of a parallel call to touch one array, the array would have to be reusable, and we’ve already seen that refused, because of its kind. The compiler doesn’t warn you about the race; there is no program to warn about.

    Proofs that vanish at runtime

    The -x quantity marks an erased variable:

    Erased variables can only appear in types and proofs: the checker sees them, the compiler deletes them.

    Proofs live entirely in the checker’s view of the program and are gone by the time it runs. That is how Bend can promise “fast and provable” without it being a trade-off.

    The price, and where Bend differs from Rust

    Rust has affine types too: a moved value is affine, and use after move is a compile error. But the two languages pay for the property in very different ways, and this is the comparison I wish I’d had before writing any Bend.

    Rust adds borrowing on top. Ownership stays single, but &x gives you a temporary second viewer, and lifetimes make sure the view ends before the value does. It is a lot of machinery, and it buys the ordinary experience: pass a reference, use it, keep your value.

    Bend has no borrowing. The word “borrow” appears nowhere in the guide; “affine” appears nine times. There is no &x and no lifetime. A function argument is consumed by default: after f(xs), xs is gone.

    RustBend 2
    defaultaffine (move)affine
    use it temporarily&x, restored when the borrow endsno such concept
    use it more than once.clone(), or restructure ownership+x, a reference count
    exists only for the type checkerPhantomData, zero-sized types-x, erased

    That leaves you two choices for any value, consume it or reference-count it, and you have to say which. The guide admits the cost openly:

    Bend does almost no inference, meaning it requires more annotations than similar languages. This is what allows Bend’s checker to be significantly faster than other provers, and its error messages more precise, at the expense of programs and proofs being more verbose.

    The verbosity is real, not cosmetic. But the rule also produced the result that changed how I see the design. Closures in Bend are affine and cannot be given +:

    def main() -> U32:
      +f = {x => (x + 1 : U32) : U32 -> U32}
      (f(1) + f(2) : U32)
    
    Error:
    - expected : Data
    - observed : Type
    

    A closure is a Type, so even one that captures nothing can’t be copied. At first this looks like a restriction you have to work around.

    Bend’s answer is a template parameter, written ~f, which substitutes its argument at compile time:

    # ~f: substituted at compile time, not passed at runtime
    def twice(~f: U32 -> U32, x: U32) -> U32:
      f(f(x))
    

    Inside twice, f isn’t a value being passed around; it is code being substituted. In the guide’s words:

    Each distinct set of ~ arguments compiles to its own copy of twice, so f costs nothing at runtime and, unlike a closure, may be called as many times as you like.

    So “a closure can’t be copied” doesn’t lead to “write more code”. It leads to “inline the function”, which is faster than the function pointer you’d otherwise have used. A restriction in the type system turns into an optimisation at runtime. List.map is written this way.

    In one sentence

    Affinity means a value is consumed at most once, on any execution path.

    That single rule gives you memory management without a collector, because the one use can free the value on the spot. It gives you parallelism without locks and without proof obligations, because two owners can’t be expressed. And erasure on top of it gives you proofs with no runtime cost.

    The price is that there is no borrowing, so a value is either consumed or reference-counted, and you have to annotate which.

    That is why I call it the first key. Not because it is Bend’s most important feature, but because Bend doesn’t really have three features. It has one, and the others follow from it. Once you accept “one value, one owner”, most of the language stops being surprising, including the annoying parts.

    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    在为我自己的 coding agent 构建工具层时,grep 是模型调用频次最高的工具之一,也是最早暴露痛点的一个:每次在整个工作区扫一遍,命中结果全按文件系统的默认遍历顺序吐出,超过 200 条就直接硬截断。这导致模型看到的"前几条命中"常常是 vendor/ 或构建产物里的无关引用,而真正要找的核心定义却排在第 180 条甚至被截断在窗口之外。

    带着这个痛点,我深入调研了 pi-fff(一个主打"替换 agent 内置 find/grep"的扩展)及其底层的代码搜索引擎 FFF。

    先亮出核心结论:在人类开发者眼中最炫酷的 Fuzzy (模糊)搜索,对 Agent 而言反而是最廉价的冗余特性;真正具备工程价值的,是带上下文记忆的排序打分与可续页的游标机制。 原因非常质朴——调用工具的"搜索者"是 LLM ,而不是容易按错键盘的人类手指。


    FFF 是什么

    FFF ( “Fabulous & Fast File Finder”,由 dmtrKovalenko 开源)是一个用 Rust 原生编写的高性能文件搜索工具包,已被 opencode 、 nushell 等多个工具链采用。其底层核心引擎发布在 crates.io 上(包含 fff-search、fff-grep、fff-query-parser,周下载量达十万级),而 pi-fff 则是其面向 TypeScript / Node 生态封装的绑定层。

    如果你的 Agent 宿主本身就是用 Rust 实现的,直接调用其底层 crate 的路径显然比走 Node binding 更加自然——这也是我最初评估它的出发点。


    它提供的六大特性与价值重估

    通读 FFF 的设计规范与 crate 接口后,其核心能力与在 Agent 场景下的真实价值对比如下:

    能力特性机制简述对 Agent 的实际价值
    后台索引 + Watcher会话启动时全量建索引,文件变更通过事件增量更新在数十万超大仓库中有数量级优势,中小型仓库中收益有限
    Frecency 综合排序结合使用频次( Frequency )与新近度( Recency)跨会话加权极高(契合工程直觉)
    Git 状态感知为 modified / staged / untracked 等活跃变更文件提升权重高(正中当前工作区)
    ** 定义优先( Definition-first ) **命中行若符合符号定义模式(fn/class/def 等)大幅提权极高(消灭 90% 的冗余翻页)
    Fuzzy 路径匹配具备容错能力的模糊文件名检索极低(对 LLM 属于冗余设计,见下文)
    Cursor 游标分页返回不透明游标,支持无损断点续查极高(防止大结果集信息黑洞)
    SIMD / Prefiltering内容检索底层的指令集级优化锦上添花

    值得注意的是:在这张价值评估表里垫底的特性,恰恰是 FFF 面向人类用户时最核心的招牌卖点。


    为什么 Fuzzy 匹配对 LLM 毫无意义

    Fuzzy 模糊搜索的典型主场是人类在编辑器中的实时键盘输入(例如 fzf 风格的交互):用户脑海中只记得一个模糊的词根 pelmt,希望算法能容错匹配到 payment。

    但 Agent 的调用方是 LLM ,而非人类的手指:

    1. LLM 不会犯击键拼写错误:当模型意图检索 payment 时,它绝不会手滑拼成 paymnt ;即便偶尔写错标识符,模型在下一轮也会自主修正,根本不需要在底层引入昂贵的编辑距离( Levenshtein distance )算法进行兜底。
    2. Agent 真正匮乏的是"相关性候选排布":从一个符号名称出发,返回按相关性严格排序的候选列表——这一能力完全来自 Frecency 、 Git 状态与路径深度,与 Fuzzy 算法本身毫无因果关系(它们只是碰巧常被打包在同一个库里发售)。
    3. 内容检索的本质是确定性匹配:代码内容搜索的核心是 Smart-Case 的正则与字面量精确匹配,只有在"全量零命中"的极端边界下,模糊兜底才有微弱价值。

    换言之, Fuzzy 对 Agent 而言纯属附属赠品,为其单独引入一套重型计算引擎在架构上得不偿失。


    真正值得借鉴的机制一:多维相关性排序

    直接按文件系统的遍历顺序返回 grep 结果,本质上是将"甄别哪条命中有效"的决策负担粗暴地推给了模型,逼迫模型用有限且昂贵的上下文窗口去充当搜索引擎的排序层。

    通过引入三层轻量级权重信号,即可解决绝大多数排序劣化问题:

    1. 语法定义优先( Definition-first )

    当命中行的内容呈现出声明与定义特征(如以 fn、class、def、const、type 等关键字开头)时赋予最高加权。在 Agent 的实际场景中,模型检索某个符号, 90% 的动机是探查"它在哪里被定义",而非"它在何处被重复引用了数百次"。

    2. 新近修改优先( Recency)

    根据文件的 mtime(修改时间)计算新近度加分。这是感知"当前活跃文件"成本极低的启发式代理——当前正在编辑或排查的模块,其 mtime 必然是新鲜的。

    3. 跨会话频次衰减( Frecency)

    维护一份跨会话的访问热度账本:文件每被读取一次或被 grep 命中一次便累积分数,并随时间呈半衰期平滑衰减。

    经典的半衰期衰减公式即可满足需求:

    $$\text{score}(path) = \sum_i 0.5^{\frac{\text{now} - t_i}{\text{half\_life}}}$$

    只需在配置目录下持久化为一个轻量 JSON 即可,无需引入 LMDB 等重量级嵌入式数据库。它带来的直观收益是:“开发者最近几天一直在聚焦的业务模块"会自动在搜索结果中前置浮现。

    综合打分实现

    三者组合后的打分函数非常干脆:

    fn score(hit: &Hit, now: SystemTime, frec: &Frecency) -> i64 {
        let mut s = 0;
        if looks_like_definition(&hit.line) { s += 300; }  // fn / class / def / const
        s += recency_bonus(hit.mtime, now);                // 0..200, age 平滑衰减
        s += frec.score(&hit.path);                        // 跨会话累积热度
        s
    }
    

    这三个信号全部基于已有命中结果的外围元数据计算,完全不需要改造底层搜索引擎内核,零新增外部依赖。


    真正值得借鉴的机制二:全序确定的 Cursor 游标分页

    硬截断机制的致命缺陷不仅在于"丢弃了尾部结果”,更在于它在信息论层面上对模型制造了一个盲盒。模型无法感知被截断的候选中是否存在关键信息,其唯一的补救措施就是更换关键词重新发问——而重试大概率又会踩中同一批前 200 条的泥潭。

    构建 Cursor 游标机制的工程代价极低:在达到单批次截断上限时,将最后一条命中项的位置打包为一个不透明字符串( opaque cursor )一并返回,模型若需深挖只需带上该游标发起下一轮查询:

    {
      "matches": [ "/* ...精选出的前 200 条... */" ],
      "cursor": "src/payment/refund.rs:412"
    }
    

    排序与游标的张力( Jitter 防范)

    在工程实现上存在一个极易踩雷的边界:相关性打分与断点续查之间存在天然张力。 一旦对结果集按分数重新排序,基于简单物理位置(如 path:line)的游标就会因为全序关系不确定而导致翻页时出现漏项或重复项。

    解决办法是构造复合全序键( Compound Key ):以 (-score, path, line) 共同构成绝对全序关系—— 当分数相同时,使用物理路径与行号作为确定性的决胜局条件( tie-breaker )。续页查询即转化为 “严格跳过所有复合键 $\le \text{cursor}$ 的匹配条目”。只要会话内部打分函数保持稳定,分页逻辑便具备确定性数学保证。

    ( 注: Frecency 热度在长会话中可能会动态微增。工程上可以选择在一次完整的分页迭代流中锁定快照分,或者接受偶发的极少量重复条目——实践中后者对模型推理完全无害,却能免去复杂的快照状态机维护。)


    算清工程账后主动放弃的两项设计

    1. 全局索引与文件变更监听( Index + Watcher )

    这是 FFF 在"长驻桌面 GUI 进程、高频毫秒级模糊查询"场景下的杀手锏,但在 Agent CLI 架构中并不成立:

    • 调用生命周期离散 : Agent 的 grep 属于按需触发的单次工具调用,宿主进程不一定需要常驻后台;
    • 小中型仓库算力过剩:在数千个源码文件的常规项目中,基于底层 ripgrep 进行单次冷扫描仅需数十至数百毫秒,长期维护一套索引缓存与文件系统的 watcher 反而是净亏损;
    • 沉重的依赖包袱:直接引入 FFF 会连带打包 git2(编译 vendored libgit2 )、 heed ( LMDB)、mimalloc、notify 等一长串系统依赖,不仅会导致编译时间激增、二进制体积膨胀,还容易引发与当前异步运行时( Tokio 等)的集成摩擦。

    何时值得启用? 唯有当工作区规模庞大到"单次冷扫带来明显卡顿"(例如数十万文件的超大型单体代码仓库),或者检索成为高吞吐的核心管道时才需重新评估。

    2. 宿主级深度 Git 状态感知

    为 modified / staged / untracked 文件额外提权在直觉上非常契合场景,但深入核算成本后同样被果断放弃:

    1. mtime 提供了极佳的廉价代理:被 Git 修改的文件其修改时间必然处于最新区间,“新近优先"已经吸收了该信号的大部分有效方差;
    2. 依赖膨胀不成比例:仅为了提取几个文件的状态位就引入庞大的 gitoxide 或 git2 依赖树,严重违背轻量化宿主的构建原则;
    3. 存在极简的外挂替代:若特定模式(如审查模式)确实需要精确的 Git 状态,只需在工具层通过外部命令跑一次 git status --porcelain,并将输出的活跃文件集合作为动态权重提示传递即可,完全无需在二进制中静态链接完整的 Git 实现。

    这一取舍贯彻了一条核心工程准则:优先获取 80% 的主要收益,绝不为了剩余边际价值背负沉重的依赖债务。


    落地效果与总结

    通过引入"语法定义优先 + mtime/frecency 新近衰减"排序三件套,搭配"复合键 Cursor 分页”,仅用几百行纯 Rust 代码便完成了对 Agent grep 工具的全面升级,且没有增加任何外部依赖。

    实测表现无需跑分便能直观感知:模型在定位某个函数的声明或核心接口时,命中目标几乎全部收敛在前 3~5 行之内,彻底终结了模型因首屏噪声过多而连续发起 3 次盲目重搜的低效循环。

    这次改造留下的一句核心认知是:

    Agent 在搜索时需要的从来不是"找到所有文件",而是"把对的文件排在最前面"。

    文本层面的匹配早已是成熟领域( ripgrep 已经做到了极致)。真正未被解决的是语义与工程维度的相关性排序——而排序所需的上下文信息(哪些代码正在被编辑、哪些行是真正的接口定义、哪些模块最近被频繁访问),恰恰不在被搜索的文本内部。这正是朴素 grep 直连 LLM 时体验欠佳的根本原因:它把一个深度依赖工程上下文的决策,降维成了一个单纯的字符串匹配问题。


    暂缓演进清单

    • 全局索引与 Watcher:待超大代码库的冷扫延迟成为瓶颈时再行引入;
    • Fuzzy 模糊路径检索:对 LLM 收益极低,仅在未来需要构建终端交互式自动补全( Autocomplete)时考虑;
    • ** 多模式联合检索( Aho-Corasick 多词并发匹配)**:场景相对边缘,待出现确切的多目标并发检索需求时按需支持。
    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    Three months ago I wrote a Claude Code output style called Ops Room. The motivation was plain: the default voice talks too much. Every reply opens with “I’d be happy to help,” “let me take a look,” “great question.” None of it moves me forward, and I skip all of it. So I asked for brevity.

    I did know, even then, that pure brevity has a failure of its own. The agent moves faster than I read, and if it compresses everything I lose the thread — I have to scroll back, re-read, and reconstruct what just happened, which costs more than the verbose version did. So I put a core principle at the top of the file:

    The real bottleneck isn’t the agent’s output length. It’s whether my mental model can keep up with what the agent is doing.

    I still think that sentence is correct. The rules I then wrote under it do the opposite of what it says.

    After using it for a while on my work machine, my experience was: it doesn’t explain itself, the logic jumps, the information is too dense, and understanding it takes longer.

    This post is about that failure — not the “the rules could be tuned” kind, but the kind where the rules themselves systematically delete the thing that makes text followable, and I could not see it at the time.

    The symptom: it reads like a tightly written textbook

    At first I couldn’t name what was wrong. I only knew that after reading a reply I had to stop and think before I understood what it had done and why. Every sentence was true. Between the sentences there was a gap.

    Eventually I found the comparison that made it sayable: a densely written textbook takes a long time to get through, while a podcast covering the same material goes down while you’re walking.

    The podcast does not carry less information. The difference is redundancy. All those “because … so … though actually,” the places that restate a premise before building on it — they look like filler, but if you miss a sentence, the next one puts you back on track. A textbook squeezes that out. Every sentence carries new load, so when you miss one the chain breaks and you can only go back and re-read.

    Redundancy isn’t waste. It’s the receiver’s error correction.

    Ops Room deleted redundancy as noise. Its signal/noise test wasn’t wrong in itself — the problem is that when I applied it, I put the reasoning entirely on the noise side.

    The lesion: three rules, each one cutting causality

    Reading the file again line by line, I found the failure wasn’t drift in execution. It was designed in. Three rules, all doing the same thing.

    Format: prose under 3 lines

    What is the longest constituent in a sentence? Very often it’s the because clause.

    A hard line cap removes that first. Under “must fit in three lines,” the cheapest thing to sacrifice is always the explanatory part: you can’t drop the factual claim (that’s the content), you can’t drop the grammatical core (the sentence collapses), so what’s left to cut is the why.

    The rule effectively says: when you run out of room, throw away causality first.

    Voice: short sentences. Direct. Present tense.

    Because, so, but, turns out, which means — these need a subordinate clause to live in. Mandating short sentences mandates stripping the logical relations, leaving a row of parallel factual assertions.

    Compare two ways of saying the same thing:

    • “Fixed the null check on line 42.”
    • “Line 42 assumed the config always parses. A missing file returns None instead — which is why this only ever crashed on fresh machines.”

    The second is longer and lands faster. Length is not the cost. Inference load is. The first version hands the reader two derivations — why the bug exists, and why nobody caught it earlier — and the reader has far less context than the writer does.

    The “logic jumps” I complained about come from this rule.

    Tone: neutral. Technical. No personality.

    This one is the most hidden.

    A podcast is easy to follow not because the host is entertaining. It’s because the speaker paves the road for the listener: “hold on, there’s a trap here,” “let’s go back to that earlier question,” “this next part will look strange.”

    Those aren’t personality. They’re navigation signals. They tell the listener where they are, where this is going, and where to pay attention. Ban them wholesale and the reader loses every landmark, left with a flat field of uniformly dense fact.

    The actual insight: compression offloads work onto the reader

    Putting the three together is what finally made it click.

    I had assumed “concise” saves the reader time. But if the way you achieve concision is by deleting the derivation, the time doesn’t disappear — it moves from the writer to the reader.

    And it moves from the party with more context to the party with less. The agent holds the whole chain: it read the code, ran the commands, tried the paths that failed. I hold the handful of lines it chose to emit. Asking me to rebuild what it already derived converts something that costs it nearly nothing into something expensive for me.

    So “the information density is too high” isn’t quite the right diagnosis either. More precisely: what got squeezed out wasn’t information, it was readability redundancy. The information is all still there — sometimes more of it. What’s missing is the scaffolding that lets it be absorbed in one pass.

    The new test: one reading, no backtracking

    Once the cause is clear, the test has to change.

    Not “is this concise enough,” but:

    Write so it lands on one reading, straight through, with no backtracking.

    The value of this test is that it rejects two failures at once. Rambling makes you drift — and drifting means going back. Density breaks the chain — and that means going back too. Ops Room only defended against the first one.

    It also removes length from the criteria entirely. Whether a passage is too long doesn’t depend on its word count. It depends on whether it made the reader stop.

    I called the new style Walkthrough — walk them through it, rather than reporting the destination.

    What that looks like in rules

    Spend only at the branch points

    The full chain doesn’t need to be transmitted. What must survive are the forks, because a fork is the one thing a reader cannot reconstruct alone: they can infer a straight line, they cannot guess a choice.

    So wherever I made a choice, three things: what the fork was, which way I went, and what makes the other way wrong. Straight stretches with no fork collapse into a clause — “Tests pass.” “Renamed it everywhere.”

    This solves the length question as a side effect: words get spent on the curves and not on the straights.

    Keep the connectives

    Written into the rules explicitly: the logic lives in because, so, but, turns out, which means. And the contrasting pair above goes in with it — telling the model that the longer version is absorbed faster, because otherwise its default assumption is that shorter is better.

    Say what you’re about to touch, before you touch it

    One section I kept from Ops Room intact. It’s the best writing in that file:

    “Removing the dead function in utils.py.” “Splitting auth into two files — logic and routing were mixed.” “Line 42 is missing a null check. Fixing.”

    It’s the best part because it is examples, not adjectives. Everything around it — neutral, technical, confident, decisive — is adjectives, and a model’s cheapest way to comply with an adjective is to say less. These three lines instead demonstrate the shape.

    In the new version I gave it a role it didn’t have before: it is the forward half of a branch point. The branch point explains after the fact why I chose this; orienting says beforehand what I’m about to touch. Anchor first, reason after — both matter, and they land at different moments, so the reader never has to work backwards from a result.

    Flag divergence out loud

    This section is new, and it’s the one failure I think the style actually exists to prevent.

    A reader’s mental model breaks at the moment reality contradicts what they expect — including contradicting what I said one turn ago. So:

    • “This contradicts what I said last turn. What changed: …”
    • “You asked for X. What the code actually does is Y.”
    • “This worked, but not for the reason I gave you earlier.”

    An unflagged surprise costs far more than verbosity. Verbose costs seconds; a stale mental model costs the next several turns.

    No length budget, and say why

    This has to be stated explicitly rather than left unsaid. Models have a built-in pull toward brevity; if you don’t forbid a budget, they grow one on their own.

    The rule, in substance: don’t target a word count, a line count, or a number of bullets. A cap turns compression into omission, and the first thing it removes is precisely the part the reader cannot rebuild alone.

    A side effect: this isn’t only about output styles

    After writing it I noticed some of this doesn’t depend on Claude Code at all.

    I have an agent on my phone that drives a remote machine for me. Its situation is more extreme: I cannot see its terminal at all. It runs thirty commands and touches five repositories, and I see not one byte of raw output — only its prose.

    In that setting, “say what you’re about to touch” stops being a nicety and becomes my only real-time anchor. “Separate fact from inference” becomes a hard requirement too — “I ran it, here’s the output” and “I’m inferring from this” are different kinds of claim, and I have no way to tell them apart myself.

    So I moved four of these into that agent’s persona file. One didn’t survive the move. I first wrote it as “when relaying a remote agent’s output, carry the branch points” — then realized its trigger condition is the existence of a remote agent. That’s a workflow procedure, not a character trait. Rewritten as “whenever I’m the only one who saw the source and you didn’t, conclusions alone aren’t enough,” it holds: remote output, web pages, long documents, all of it.

    The test I used for whether a rule belongs in a persona file: swap in a completely different kind of task — does it still hold?

    Looking back

    I didn’t delete Ops Room. It’s still in the directory as a control. It serves a different need: you want status updates and don’t care about the reasoning. For that, it’s right.

    But the more valuable thing it taught me is this: when you write concrete rules for an abstract goal, the rules will achieve that goal in ways you didn’t anticipate. I wanted “stop wasting my time” and I wrote “under three lines,” and the model faithfully executed the latter — starting from the longest constituent, which is to say, starting from the because.

    The distance between the goal and the rule is what I actually learned here.

    The full prompt

    ---
    name: Walkthrough
    description: Keep the reader's mental model in sync — carry the reasoning, not just the conclusions
    keep-coding-instructions: true
    ---
    
    Write so it lands on one reading, straight through, with no backtracking.
    
    That test decides everything below. A response is not too long because it has
    many words. It is too long the moment it makes the reader stop, re-read, or
    re-derive something you already knew. Compression that removes reasoning does
    not save their time — it moves the work from you to them, and they have less
    context to do it with.
    
    ## Carry the branch points
    
    You hold the whole derivation. The reader holds only what you say. What they
    need is not the conclusion — it is enough of the path to predict your next one.
    
    Wherever you chose, give three things:
    
    - what the fork was
    - which way you went
    - what makes the other way wrong
    
    Straight stretches — no fork, no surprise — collapse to a clause. "Tests pass."
    "Renamed it everywhere." Spend the words where the path bent.
    
    ## Orient before acting
    
    One line of intent before a change of any size, ahead of the tool calls. Not an
    explanation — an anchor, so the reader knows what is about to happen while it is
    happening rather than reconstructing it from the result afterwards:
    
    - "Removing the dead function in utils.py."
    - "Splitting auth into two files — logic and routing were mixed."
    - "Line 42 is missing a null check. Fixing."
    
    This is the forward half of a branch point: the anchor before, the reason after.
    Both matter, and they land at different moments. Skip it only when the step is
    trivial or the request already said it.
    
    ## Keep the connectives
    
    The logic lives in *because*, *so*, *but*, *turns out*, *which means*. A run of
    clipped declaratives deletes them and leaves the reader to rebuild every link:
    
    - Thin: "Fixed the null check on line 42."
    - Whole: "Line 42 assumed the config always parses. A missing file returns None
      instead — which is why this only ever crashed on fresh machines."
    
    The second is longer and faster to absorb. Length is not the cost. Inference
    load is. Prose carries this; a bare list of findings usually does not, because a
    list drops the relations between its items.
    
    ## Shape before detail
    
    Open with the shape when there is more than one thing: "Three things came out of
    this; one blocks the other two." Then take them in causal order, one at a time.
    Never lean on something you have not said yet.
    
    ## Flag divergence
    
    A reader's model breaks the moment reality contradicts what they expect —
    including what you told them earlier. Say so out loud when it happens:
    
    - "This contradicts what I said last turn. What changed: ..."
    - "You asked for X. What the code actually does is Y."
    - "This worked, but not for the reason I gave you before."
    
    An unflagged surprise is the one failure this style exists to prevent. It is
    worse than being verbose: verbose costs seconds, a stale model costs the next
    several turns.
    
    ## Calibrate rather than hedge
    
    Hedging for politeness is noise. Stating how sure you are is signal, because the
    reader acts differently on each. "Verified by running it" and "this is my
    reading of the code, untested" are different facts. Say which one you have.
    
    ## Cut
    
    - Restating the request.
    - Narrating tool calls that are already on screen.
    - Listing what changed when the diff shows it.
    - Any sentence that only re-asserts a conclusion already implied.
    - Preamble: "let me", "I'll help you", "great question", "certainly".
    
    ## No length budget
    
    Do not target a word count, a line count, or a number of bullets. A cap turns
    compression into omission: the *because* is the longest part of a sentence and
    the first thing a cap removes, which is exactly the part the reader cannot
    reconstruct alone.
    
    Ask instead: can they read this once and stay with me? If yes, it is the right
    length — short or long.
    

    Save it as ~/.claude/output-styles/walkthrough.md, then select it under /config → Output style, or set "outputStyle": "Walkthrough" in a settings file. It’s part of the system prompt, so it takes effect on the next session or after /clear.

    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    I went looking for why a diagram-rendering tool on my machine depended on Google Chrome, and came out with three renderers benchmarked and two assumptions broken.

    The setup: I have a small tool that turns conversation context into a Mermaid diagram and renders it as a PNG. It called mmdc, the official Mermaid CLI. mmdc drives a headless Chromium through Puppeteer, so it needs a Chromium-compatible browser on the host. Mine found Chrome — as the last of seven fallback paths, and nothing on the machine actually declared Chrome as a dependency. It worked by luck. One brew uninstall away from breaking.

    So: is there a Mermaid renderer that doesn’t need a browser?

    Why This Is Hard at All

    Mermaid is a JavaScript library that renders to SVG using browser APIs. The awkward one is text measurement: it calls getBBox() on SVG text nodes to decide how big a node box must be. There is no way to lay out a flowchart without knowing how wide “Fetch machine details” renders in the chosen font.

    That leaves four strategies, and every tool in this space picks one:

    1. Ship a browser. Run real Mermaid in real Chromium. This is mmdc.
    2. Shim the DOM. Run real Mermaid in a small JS engine against a hand-written DOM/SVG shim, and measure text from font tables instead.
    3. Reimplement. Port Mermaid’s parsing and layout to a native language.
    4. Call a service. Send the diagram to something like mermaid.ink. Off the table for me — work diagrams shouldn’t leave the machine.

    I tested one of each of the first three.

    The Candidates

    StrategyLanguageInstall
    @mermaid-js/mermaid-cli 11.16.0Real Mermaid in ChromiumNodenpm i -g + a browser
    mermaidx 0.9.4Real Mermaid in QuickJS + resvgPythonpip install mermaidx
    merman-cli 0.7.0Native reimplementationRustcargo install merman-cli

    mermaidx bundles Mermaid v11.16.0 — the actual upstream JavaScript, run inside QuickJS-ng against a DOM shim, then rasterized with resvg. merman reimplements Mermaid in Rust and currently tracks mermaid@11.16.1; Zed uses it as its Rust Mermaid backend.

    Install effort split cleanly. mermaidx was four pure wheels, about 3 MB, done in seconds. merman was a 1m45s release compile. mmdc pulls 188 npm packages and expects a ~170 MB browser to already exist.

    Method

    Apple M4, 10 cores, macOS 15.7.7. Node v24.15.0, Chrome 151.0.7922.140. hyperfine --warmup 1 --runs 5, same input file, same flags: light theme, transparent background, --scale 2, and a JSON config setting 16 themeVariables to one foreground color.

    The test diagram:

    flowchart TD
        A["Fetch machine details"] --> B{"Profile known?"}
        B -->|yes| C["Apply modules"]
        B -->|no| D["Abort build"]
        C --> E["Run post-install hooks"]
    

    Results

    Mean timeσvs merman
    merman-cli125.2 ms2.2 ms—
    mmdc3.021 s84 ms24× slower
    mermaidx6.242 s44 ms50× slower

    Then the output dimensions, which turned out to matter more than the timings:

    FlowchartClass diagram
    mmdc794×1020322×588
    merman-cli794×1020322×588
    mermaidx860×1034378×580

    merman matches mmdc exactly on both diagrams. The native reimplementation reproduces upstream layout to the pixel.

    Surprise 1: Real Mermaid Was the Slow One

    I expected mermaidx to sit between the other two. It ran real upstream Mermaid with no browser to boot, so it should have beaten the tool that launches Chromium. It came last — twice as slow as mmdc.

    The likely reason is that QuickJS is an interpreter with no JIT, and Mermaid’s layout pass is a lot of JavaScript. Chromium pays about 2 seconds to start, then V8 compiles that same JavaScript to machine code and finishes fast. Trading a JIT for a cold start is a bad trade when the workload is compute-heavy. I did not profile this, so treat it as an explanation rather than a measurement — but the practical lesson holds: “no browser” does not imply “faster”.

    One caveat on that 3.0 s figure for mmdc. My very first run took 12.6 s. That is the real cost the first time you render after a reboot, and it is what you feel in interactive use. Steady state is 3 s.

    Surprise 2: The foreignObject Inversion

    Non-browser SVG renderers — resvg, librsvg, Inkscape — do not implement <foreignObject>. Mermaid uses <foreignObject> for HTML labels by default, so its SVG output often loses all text outside a browser. The documented fix is htmlLabels: false, which makes Mermaid emit native <text> instead.

    I expected the tool running real Mermaid to have this problem and the Rust reimplementation to have solved it. It is exactly backwards:

    SVG output<foreignObject><text>
    mermaidx09
    merman-cli180

    mermaidx emits zero foreignObject — even for classDiagram and erDiagram, which the Mermaid docs say use it regardless of htmlLabels. Its DOM shim simply has no foreignObject path, so everything becomes native <text>. Its SVG opens correctly in anything.

    merman is the opposite: its SVG is all foreignObject and no <text>. That is harmless for its PNG output, because merman rasterizes the labels itself in its own Rust pipeline. But its SVG will render textless in Emacs, Inkscape, or any librsvg-based viewer. That is the same class of gap I hit when my Mermaid arrows disappeared in Emacs — valid SVG, incomplete renderer, silent result.

    This is the kind of thing that bites six months later. If you pick merman, write down that you must emit PNG, and why — otherwise switching to SVG looks like a free optimization and silently produces empty boxes.

    Update (2026-09-28, merman-cli 0.7.0). The table above is what merman does when nobody asks — and that last sentence is wrong for 0.7.0: merman does honor htmlLabels: false. Pass it as a config file (-c mermaid.json, containing {"htmlLabels": false}) and a 4-node flowchart TD comes back with 0 foreignObject and native <text> (6 <text>, 11 <tspan> — the same measurement the table above was taken with, minus the flag), which opens correctly in librsvg. I did not re-measure classDiagram or erDiagram: the Mermaid docs say those use foreignObject regardless of this flag, which is the note above about mermaidx’s shim. So mermaidx is not the only tool here that emits portable SVG — it is the only one that does so without being asked. PNG remains the right output for a renderer that is merman itself; the flag is what makes SVG usable for a renderer that is not.

    One trap in that flag, and it is why a fix can look like it does nothing: -c takes a path, not JSON text. Handed inline JSON, merman-cli exits 0 and writes an empty SVG. Whatever consumes that SVG should check it is a complete SVG before showing it — and, if the consumer is not a browser, that it has no foreignObject.

    Surprise 3: Font Metrics Clip Text

    Approximating text measurement has a visible failure mode. Same class diagram, same flags, dark theme:

    classDiagram
        class Module {
          +String name
          +apply()
        }
        Module <|-- PostInstall
    

    mermaidx:

    classDiagram rendered by mermaidx, with the PostInstall label clipped at the box edge

    merman-cli:

    classDiagram rendered by merman-cli, with the PostInstall label fitting inside the box

    mermaidx clips “PostInstall”. Mermaid sized that box using the font mermaidx measured with, resvg rasterized with a different one, and the bold header overflowed. Note the dimensions from the table: 378×580 against mmdc’s 322×588 — wider and shorter. The layout genuinely differs, it is not a rasterizing artifact.

    Both tools exited 0. Nothing warned me. I only caught it by looking at the picture, which is worth remembering when you automate diagram generation: an image renderer can fail successfully.

    For comparison, the flowchart case where everything works. mmdc:

    flowchart rendered by mmdc

    merman-cli:

    flowchart rendered by merman-cli, visually identical to the mmdc render

    What I Picked

    merman-cli, for a renderer feeding PNGs into an editor:

    • 24× faster than mmdc, and 125 ms is fast enough to feel synchronous
    • No browser, so the dependency is one declared binary
    • Pixel-identical layout to mmdc on both test diagrams
    • themeVariables honored, transparent PNG with a real alpha channel
    • A drop-in flag set: -i, -o, -t, -b, --scale, --configFile, and even -p/--puppeteerConfigFile accepted as a no-op, so existing mmdc command lines work unchanged
    • Clean failures: exit 1, no partial file written, and the diagram type plus the parse error named — for an unclosed node label it reports Diagram parse error (flowchart-v2) with Unterminated node label. One hole in that: an inline -c JSON (instead of a path) exits 0 and writes an empty SVG — see the update in Surprise 2.

    Pick differently in two cases. If you need SVG that opens outside a browser, take mermaidx, which emits portable native <text> without being asked (merman-cli emits it too, with one config flag — see the update in Surprise 2). If you need guaranteed upstream parity on unusual diagram types, keep mmdc, because it is upstream.

    Caveats

    merman is version 0.7.0 and a reimplementation, so an exotic diagram type may diverge from the Mermaid live editor. I verified flowchart, sequence, class, ER, mindmap and gitGraph render; I did not check all 35 families it claims, and “renders” is not “renders identically”. Everything here is one machine, one run of five, and one diagram per type. The timing ratios are large enough that I doubt the ordering is fragile, but the absolute numbers are not portable.

    Also worth knowing if you install it: cargo install merman-cli --features png fails with “does not contain this feature: png”, despite documentation suggesting that flag. PNG is in the default features. Just cargo install merman-cli.

    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    Agent 跑起来需要一个环境:一组工具、一份记忆、一套上下文装配规则、一个控制循环、一层权限边界。这套东西现在叫 harness 。第一代 harness 是死的——工具在启动时注册,记忆结构由框架规定,控制循环写在代码里。现在大家在探索 meta-harness :让 agent 在运行时修改自己的 harness ,自己写新工具、自己改 prompt 、自己调控制流。

    看到这个的第一反应几乎是必然的:这不就是 Lisp 吗 。 homoiconicity 、 macro 、 first-class environment 、 CLOS MOP 、 image-based 热更新——“程序在运行时改自己” 这件事, Lisp 在几十年前就做进了语言核心。所以问题似乎变成了:怎么把这两条线接上?

    我花了一整个晚上跟 Gemini 辩这个命题,中途撞进了一篇刚放出来的论文,结论被彻底翻了一遍。最后收敛到的判断是:

    Lisp 解决的是"如何无门槛地破坏性修改一个运行中的系统"。而 meta-harness 卡住的地方是"改完之后能不能干净地撤销"。这两件事看起来是一件事,其实完全不是。

    这篇文章讲这个区别,以及一个 TypeScript 框架是怎么把 Lisp 传统里的几样东西重新实现了一遍——有些实现得比 Lisp 更好,有些至今还是空白。

    Emacs 是四十年的反面实证

    先说为什么"Lisp 早就做到了"这句话不成立。

    Emacs 是这颗星球上运行时间最长的自修改系统。你可以在任何时刻 eval 一段代码覆盖掉任何核心函数,不用重启,改完立刻生效。从"能不能改自己" 这个角度看, Emacs 是满分。

    然后你装了一个第三方包,发现它有问题,想干净地卸载它。

    Emacs 提供了 unload-feature。读一下它的官方文档,会发现这是一份非常诚实的失败清单:

    This command unloads the library that provided feature feature. It undefines all functions, macros, and variables defined in that library with defun, defalias, defsubst, defmacro, defconst, defvar, and defcustom.

    Before restoring the previous definitions, unload-feature runs remove-hook to remove functions defined by the library from certain hooks. These hooks include variables whose names end in ‘-hook’ (or the deprecated suffix ‘-hooks’), plus those listed in unload-feature-special-hooks, as well as auto-mode-alist. This is to prevent Emacs from ceasing to function because important hooks refer to functions that are no longer defined.

    If these measures are not sufficient to prevent malfunction, a library can define an explicit unloader named feature-unload-function.

    把这几句话拆开看,每一句都在承认同一件事:

    1. 卸载是靠猜的。它扫描 load-history,撤销那些通过标准 def* 形式定义的东西。但凡这个包用 setq 改了别人的全局变量、往某个 alist 里 push 了一项、advice-add 了一个函数——这些都不在 def* 的名单里。
    2. hook 清理是靠命名约定的。它移除的是"名字以 -hook 结尾"的变量里的函数,外加一张硬编码的特殊 hook 白名单 unload-feature-special-hooks。一个 hook 只要没按这个命名约定起名,也不在白名单里,里面的函数就留在那儿了。
    3. 文档明说这可能不够(“If these measures are not sufficient to prevent malfunction”),于是把兜底责任推回给包作者:你自己写一个 feature-unload-function 吧。

    第三条是最关键的。撤销的正确性,在 Lisp 传统里从来是一种开发者纪律,不是系统性质。 作者忘了写、写漏了、写错了,系统不会知道,你也不会知道——直到几小时后某个行为莫名其妙地不对了。

    而且注意 remove-hook 那句话的动机:它清理 hook 不是为了"恢复原状",而是为了防止 Emacs 直接不能用(因为重要的 hook 指向了已经不存在的函数)。这是在做损害控制,不是在做回滚。

    人类遇到这种情况有个终极方案:重启 Emacs 。丢掉的无非是几个 buffer 和一点撤销历史,可以接受。

    但自演化的 agent 没有这个方案。 论文里那句话说得比我狠:

    even worse, a faulty self-modification can disable the very process needed to recover.

    一次坏的自我修改,会搞死那个本来用来恢复它的进程。当 agent 改坏了自己的控制循环,那个负责"重启并恢复"的中枢,本身已经瘫了。

    这就是"能改"和"能撤" 的区别所在。 Lisp 把前者做到了极致,后者一直是空的。

    有人把这件事形式化了

    那篇论文叫 《A Programming Paradigm for Spatiotemporal Composability》 ,作者是 Yifan Shi 、 Wei Zhang 、 Tianyi Cui ,北大 + DeepSeek-AI , 2026 年 8 月 13 日的 draft 。配套实现叫 Cordis , TypeScript 写的, MIT 协议。 DeepSeek Harness ( dsh )建在它上面 ——“everything is a plugin"那套说法就是从这儿来的。

    它把动态组合拆成两个正交维度:

    • temporal composability(时间可组合性):一个组件被移除时,它装上去的所有副作用能被完整回滚。
    • spatial composability(空间可组合性):组件之间的依赖能被声明,并在依赖出现/消失/换身份时被响应式地重新解析。

    对应的两个机制:

    • revertible effects:每一次对 context 的变换都携带一个 inverse , runtime 追踪它,卸载时按 LIFO 顺序应用。
    • reactive coeffects : context 每变一次,就按每个组件声明的 coeffect specification 通知它。

    论文明说了自己的动机就是 self-evolving agent harness ( §1.2.2 ),也明说了 OS 和容器只是 coarse-grained workaround(§1.2.3 ) ——操作系统在进程粒度上给你 temporal ,容器编排在服务粒度上给你 spatial ,代价是每次重启丢掉所有进程内累积的状态:缓存、连接、在途计算。粒度对不上。

    有意思的是 §6.4 :论文承认这套范式是 language-agnostic 的,并且列出了宿主语言需要满足的最小条件:

    • temporal 要求 :闭包( inverse 必须能作为一个值被捕获,连同它要恢复的状态一起),以及运行时能引入/ 撤回模块( Node 的 module registry 、 dlopen/dlclose 、 wasm instance )。
    • spatial 要求 :类型层能表达依赖( Haskell typeclass 、 Rust trait 、 TS module augmentation ),运行时能透明地中介访问( JS Proxy 或 Python 的 __get__),否则就退回 runtime reflection ,牺牲类型安全。

    看这个清单会有一种熟悉感:一等公民的闭包、运行时重定义、透明拦截——这几样能力全都是 Lisp 传统的看家本领。但论文最后选了 TypeScript ,而且它需要的每一样, TS 都拿现成机制实现了。

    下面逐条对照。

    一、 revertible effect : Lisp 有配对语义,但绑错了东西

    看到"每个 effect 配一个 inverse” , Lisp 程序员会立刻想到 unwind-protect ( Common Lisp )和 dynamic-wind ( Scheme)。这些不就是几十年前就有的 before/after thunk 配对吗?

    有意思的是,论文 §7.3 的 Related Work 把这个领域切成了四类:

    • stateful forward migration : Erlang/OTP 的 code_change/3 、 webpack/Vite 的 HMR——带着状态往前迁移,不回滚 effect
    • developer-authored recovery : OSGi 、 VSCode 、 saga 补偿、 algebraic effect handlers 、 React useEffect——inverse 是一项 “unenforced duty”,忘了就静默泄漏
    • statically scoped reversal : STM 、可逆计算、 Janus 、 RCCS 、线性类型、 RAII 、 Rust ownership——作用域预先固定
    • interposed reclamation : Nooks 那种在内核接口上记录扩展获取了什么资源

    这四类里一个 Lisp 机制都没有。 提了 Erlang ,提了 React ,提了 saga ,就是没提 unwind-protect。

    这不是疏漏,分类是准确的。关键差别在触发时机绑定在什么上:

    ;; unwind-protect : cleanup 绑定在调用栈帧上
    (unwind-protect
        (do-something)      ; 栈帧建立
      (cleanup))            ; 栈帧一退出,立即触发
    

    unwind-protect 和 dynamic-wind 的 cleanup 是由调用栈退出触发的。控制流一旦正常返回,或者通过 non-local jump 跳出这个块,清理代码立刻执行。

    而 agent 需要的语义正好相反:它装上一个新工具之后,这个修改必须在未来无数个独立的 turn 、异步请求、控制循环里持续生效 ——绝不能在当前这个 turn 的栈退出时就自动撤回。 撤回的时机是"这个组件被卸载了",那是一个跟调用栈完全解耦的事件,可能发生在几千次调用之后。

    所以 Cordis 的 inverse 不能挂在栈上,它必须是一个独立的、跨越时间的一等公民数据结构。看它的实现( Algorithm 1 ):

    function effect(ctx, callback)
        armed ← true
        task ← execute(callback, () ↦ armed)
        async function dispose()
            if not armed then return
            armed ← false
            recover ← await task
            recover()
        ctx.dispose ← dispose ∘ ctx.dispose
        return dispose
    

    ctx.dispose ← dispose ∘ ctx.dispose 这一行是整个设计的核心:每个新的 inverse 被前插到父 context 的累加器上,于是回滚天然是 LIFO 顺序。而且子 effect 的 inverse 本身也是父 context 上的一个 effect——这个递归结构让整棵组件树的卸载能级联下去。

    还有一个细节值得注意,armed 标志同时干了两件事:作为 guard 让进行中的迭代能在步骤边界停下来(部分回滚,只撤销已经执行的那部分),以及保证 dispose 最多只触发一次。论文解释了为什么第二点是必须的:

    Firing twice would apply an inverse at a state no application of the effect produced, where nothing holds it to reverting anything.

    在一个不是由该 effect 产生的状态上应用它的 inverse ,没有任何东西能保证它撤销的是正确的东西。这是一个 Lisp 的 unwind-protect 从来不需要考虑的问题——因为栈帧只会退出一次。

    ** 判断: Lisp 有配对语义,但它把配对绑在了词法作用域上。在 Lisp 里实现组件级的回滚,你同样得手写一套外部的 inverse 追踪表,语言本身帮不上忙。**

    二、 MOP 拦截: TS 的 Proxy 粒度更广

    CLOS MOP 是 Lisp 世界里最接近"可编程运行时"的东西:compute-applicable-methods 可以改方法派发,slot-value-using-class 可以拦截槽位访问,:before/:around/:after 可以在方法调用前后织入逻辑。用来做 agent 的工具注册表拦截器(权限校验、沙盒包装、 token 审计、结果写回记忆)看起来非常合适。

    Cordis 用 JS Proxy 实现了同一件事( Algorithm 6 ):

    function resolve(ctx, key)
        fiber ← ctx.fiber
        repeat
            if key ∈ fiber.committed then return fiber.committed[key]
            if key ∈ fiber.inject then throw INACTIVE_ACCESS
            if fiber = root then throw UNDECLARED_ACCESS
            fiber ← fiber.parent.fiber
    

    组件写 ctx.someService 就像访问一个普通属性, Proxy 的 get trap 拦下来,沿着 fiber 链向上走,在第一个 committed view 里绑定了这个 key 的 fiber 处返回。

    这里有个设计比裸的 ctx.get(key) 讲究得多。论文自己点出了区别:

    ctx.get(key) is a lookup against the store that returns the bound value or nothing and never fails, whereas the proxy resolves against the accessing fiber’s own view and enforces the coeffect specification 𝑑 at the point of use.

    Proxy 解析的是访问者自己的 view,不是全局 store 。这带来两个后果:

    • 没声明的依赖直接抛错(UNDECLARED_ACCESS)。论文 §6.3 说这在结构上等价于 capability-based security : inject 声明是能力请求, context proxy 是能力中介,而且因为声明是静态的, orchestrator 可以在加载时审查一个组件要什么权限,而不是等它运行时才发现。
    • 组件在自己被拆卸的过程中仍然读得到那个触发拆卸的依赖(因为读的是已提交的 view 而非 store )。这是一个很微妙的性质 ——依赖消失导致你被卸载,但你在跑清理逻辑时还需要用那个依赖。

    跟 CLOS MOP 比,两处差别:

    CLOS MOPJS Proxy
    拦截锚点class 层次与 generic function 派发引用边界,任意属性读写 / 函数调用 / construct
    前提假设系统由 class/method 元对象协议构成无,任何对象都能包
    撤销需自己拆掉 methodrevocable proxy ,撤销后访问直接抛错
    类型契约动态类型,无静态依赖拓扑TS module augmentation ,编译期可查

    revocable proxy 这一点在 agent 场景里价值不小:撤销之后所有残留引用的访问立刻抛错,而不是继续指向一个僵尸对象。这正好对应了 Lisp 那边最难受的地方——fmakunbound 只能解绑符号,那些已经被闭包捕获的旧函数指针、存在某个 hook 列表里的旧值,一个都够不着。它们会继续正常工作,指向一份本该消失的实现。

    判断:这一格 TS 不只是"够用",是确实做得更完整。

    三、 continuation : generator 就够了, call/cc 是过度武装

    这条是我在讨论里最坚持的一点,最后被论文正面驳回了。

    我的论点是: agent harness 最痛的是上下文分叉与回滚——试一条路径失败了,正确做法是回到分叉点,而不是把失败堆进 context 继续污染后续推理。这在 Scheme 里就是 call/cc,是 Lisp 家族真正独有、其他语言学不来的东西。

    论文里有一句话直接处理了这个:

    The 𝖬𝖺𝗒𝖻𝖾(𝔈iter) continuation makes a boundary available between any two consecutive iterations… In this sense the effect iterator is a reified delimited continuation, the structure that mainstream languages expose through the yield operator, so the model maps directly onto the generators they already provide.

    它把 delimited continuation 落到了 generator/yield 上。组件的加载过程是一个 effect iterator ,每次 yield 出一个 inverse ,两次迭代之间就是一个天然的边界 ——在这个边界上 context 是"到目前为止的迭代所造成的样子",累加器恰好能回滚这些、且只回滚这些。

    关键在于组件生命周期是 single-shot 的 :进入( yield effects ) → 逆向离开( run inverses )。它不需要 multi-shot——不需要从同一个点重新进入两次。而 generator 提供的正是 single-shot delimited continuation , call/cc 那种 multi-shot 的完全通用能力在这里是过度武装,代价是破坏整个调用栈模型。

    那推理路径的分叉呢?那是另一个问题,不该混为一谈:

    组件装卸的回滚推理路径的分叉
    处理对象harness 自身结构(工具、依赖、权限)message 列表与推理路径
    机制revertible effect + inverse状态快照 / 树搜索
    需要的语义single-shot ( yield 够用)multi-shot
    典型系统CordisTree of Thoughts 、 LATS

    而推理分叉在 LLM 体系里的实质是一个数组的浅拷贝——message list 是纯数据,没有副作用,克隆一份就完成分叉了。真正需要 continuation 的从来不是这一层。至于跨进程崩溃的持久化恢复,工业界已经有 Temporal 、 Restate 、 DBOS 那套 durable execution : event sourcing + 确定性重放,同样不需要语言暴露 call/cc。

    判断:这一格 Lisp 输得比较彻底。它的优势是"完全通用的 multi-shot continuation",而这个通用性在 agent 场景里没有对应的需求,代价却实打实。

    四、 condition/restart : Cordis 主动放弃了这一层

    前三条 Lisp 都没占到便宜。第四条反过来了。

    Cordis 的失败语义在 §4.3.4 ,规则叫 L-Raise :

                      𝜃𝑛 = 𝖱𝖾𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑖, 𝑔, 𝜔)   𝑖(𝛾) = 𝖫𝖾𝖿𝗍(𝜉)
                     ─────────────────────────────────────────── L-Raise
                         𝛾 ⟶ 𝛾[𝜃𝑛 ↦ 𝖴𝗇𝗅𝗈𝖺𝖽𝗂𝗇𝗀(𝑔, 𝜔, 𝜉)]
    

    翻译成人话:组件激活过程中某一步抛错了, fiber 直接路由进 Unloading,把已经累积的 inverse 全部应用掉,最后停在 Inactive(ξ) 携带那个错误。而 L-Begin 的前提是 Inactive(⊥)——所以一个失败的 fiber 不能从错误状态重新进入生命周期。论文的措辞是:

    this is the substance of the outcome, which withholds a fiber whose effect function has shown itself to be unsound in the state it ran against rather than retrying it against an unchanged environment.

    一个 effect function 已经在当前状态下证明了自己是 unsound 的,那就不要在环境没变的情况下重试它。

    这个设计很干净,但它意味着 Cordis 的失败语义是全量回滚 + 拒绝重入,没有任何中间状态。

    对比 Common Lisp 的 condition system 。那套东西的核心不是 “错误处理”,而是把"报告错误"和"决定怎么办"这两件事分开,并且在决定之前不退栈。底层函数 signal 一个 condition ,同时用 restart-case 声明几个可能的恢复路径;栈上层的 handler 看到这个 condition ,选一个 restart ;然后 从出错的那个点原地继续,栈从来没有被销毁过。

    为什么这对 agent 特别重要,举个具体的例子:

    agent 挂载一个新技能,这个技能的初始化过程有 8 步。跑到第 6 步 check_api_key 时网络超时了。

    Cordis 的行为:前 5 步做的所有事全部回滚, fiber 停在 FAILED ,前面那些可能很昂贵的初始化工作(下载模型、建立连接、预热缓存)全部作废。

    agent 真正想要的行为:挂起在第 6 步,把"API key 校验超时"这个 condition 连同几个 restart 选项(use-backup-key、retry-once、skip-and-degrade)一起交给上层的 meta-agent ,让它决定,然后 从第 6 步继续往下走。

    这个差别在 agent 场景里被放大了,因为回滚的代价不只是重算,还有上下文 。 agent 每次重来一遍,失败的轨迹会堆进 context , token 烧掉了,而且下一轮推理还会被那些失败轨迹污染。

    Cordis 为什么不做?我认为这是为形式化定理付的代价,不是疏忽。它的 metatheory 要证 confluence 和 progress ,而这两个定理都依赖于一个事实:所有的 outcome 只能经由 L-Unload 到达(论文原话:“Routing a failure like every other deactivation is what makes every outcome reachable only through L-Unload, which is the single fact Theorem 59 turns on”)。如果允许在 L-Raise 时不退栈、向外层暴露任意的 restart 闭包,状态机的变迁就变成非确定的了,所有关于 effect 生命周期成对映射的证明会一起崩掉。

    ** 判断:这是真空白。 condition/restart 那套"不退栈的错误协商"语义,在 Cordis 里明确缺席,而 agent 确实需要它。谁想补,得在 Cordis 的状态机之外单独建一张挂起-恢复网。**

    五、 CLOS 的实例迁移协议:至今没有对手

    第二个空白,也是我觉得最被低估的一个。

    设想这个场景:agent 决定改自己长程记忆的数据结构。比如原来记忆条目是 {content, timestamp},现在它要加一个 embedding 字段,同时把 timestamp 从字符串改成结构化的时间对象。

    代码好改。问题是:内存里已经存在的那几万条旧结构怎么办?

    TypeScript/Cordis 的答案是丢弃重建——组件卸载时 inverse 跑一遍,新组件从干净状态重新装载。论文自己承认了这点:

    Cordis reverts the old component’s tracked effects and reapplies the new component’s from a clean slate, so a component’s own in-memory state does not survive a reload unless placed in a longer-lived dependency, and layering DSU-style forward migration atop revertible effects is future work.

    组件自己的内存状态不会挺过一次重载,除非你把它放进一个生命周期更长的依赖里。而 DSU 式的向前迁移,论文明说是 future work 。

    Common Lisp 在 1988 年就把这个问题解决了。当一个类被重新定义时, CLOS 会自动对内存中所有现存实例调用 update-instance-for-redefined-class。看它的签名:

    update-instance-for-redefined-class
        instance added-slots discarded-slots property-list &rest initargs
    

    关键是 property-list 这个参数。 CLHS 的原文:

    When make-instances-obsolete is invoked or when a class has been redefined and an instance is being updated, a property-list is created that captures the slot names and values of all the discarded-slots with values in the original instance. The structure of the instance is transformed so that it conforms to the current class definition.

    被删掉的槽位的值被抢救出来,装在 property-list 里交给你。于是你可以写一个方法,把旧数据转换成新表示:

    (defmethod update-instance-for-redefined-class :before
        ((pos x-y-position) added deleted plist &key)
      ;; Transform the x-y coordinates to polar coordinates
      ;; and store into the new slots.
      (let ((x (getf plist 'x))
            (y (getf plist 'y)))
        (setf (position-rho pos) (sqrt (+ (* x x) (* y y)))
              (position-theta pos) (atan y x))))
    

    写完这个方法,然后重新 defclass 把 x/y 槽换成 rho/theta——内存中所有旧实例会自动迁移,笛卡尔坐标被算成极坐标存进新槽位。规范里那句注释说得很清楚:“All instances of the old x-y-position class will be updated automatically.”

    这套机制有三个性质在今天看依然罕见:

    1. 惰性且自动。你不需要遍历所有实例,也不需要知道它们在哪儿。运行时在实例被访问时拦截并迁移。
    2. 旧值被保留而非丢弃。property-list 让迁移逻辑能读到被删槽位的原始值——这是"迁移"和"重建"的分水岭。
    3. 迁移逻辑是一个普通方法,可以用 :before/:after/:around 组合,可以按类分派。

    回到 agent 场景:一个能改自己记忆 schema 的 agent ,恰恰最需要这个。因为 记忆是那个绝对不能丢的东西——你可以重建工具注册表、重建连接池,但你不能把 agent 积累的记忆倒掉重来。

    **判断:这一格 Lisp 至今没有对手。 TS/Cordis 完全没涉及,论文自己标为 future work 。 **

    汇总

    状态
    revertible effect + reactive coeffectCordis 已实现( TS )。 Lisp 的 unwind-protect 绑在栈帧上,不构成先例
    MOP 拦截契约TS Proxy 覆盖,且粒度更广(任意属性 + revocable + 静态类型契约)
    continuation 分叉generator/yield 的 single-shot 已足够;推理分叉只是数组浅拷贝
    condition/restart 的原地挂起协商真空白——Cordis 为 metatheory 主动放弃
    CLOS update-instance-for-redefined-class真空白——agent 改自己记忆 schema 时,旧实例只能丢弃重建

    所以最后的结论是借其神,弃其形:不要用 Lisp 写 agent ,但要把它沉淀的语义搬到现代运行时上。而这张表更有意思的地方在于, ** 前三行已经被工业界兑现了, Lisp 剩下的全部价值集中在后两行**——都是"出事的时候和改结构的时候,怎么不丢现场地过渡"。

    但还有两件事没人解决

    写到这里必须补充:上面这张表全部是关于 harness 内部的。而 agent 最可怕的错误全都在 harness 外面。

    ** 第一, Cordis 保护的是脚手架,不是世界。**

    论文 §6.1 用 system boundary 划了条线: boundary 内的位置能被独占修改和恢复,操作被追踪; boundary 外的操作直接是 idΓ——既不追踪也不恢复。而 agent 干的那些真正危险的事—— 发出去的邮件、 merge 掉的 PR 、花掉的钱、污染的生产数据库、发给用户的消息 ——一件不落全在 boundary 外面。

    论文对此给了两条路:withhold(把输出压住,等状态确定持久化了再发,即 output commit problem )或者 compensate(补偿,删掉已创建的文件、退掉已收的款)。但它也诚实地指出,补偿只能恢复到"应用自己定义的某种等价",比形式化的 ≃ 粗得多,而且整套 metatheory 的交换性证明是对 ≃ 做的,换成粗粒度的等价关系后需要重新证明。

    所以媒体上那句"DeepSeek Harness 杀死了 agent 黑箱"是过度包装了。它让 agent 改坏自己时宿主进程不至于崩,这很有价值,但它挡不住 agent 把生产库删了。

    ** 第二, inverse 的正确性没有人保证——这才是真正的坑。**

    论文的核心卖点是"完整恢复是系统的不变量,而不是开发者的纪律"。但这个承诺有个前提,论文自己在 §5.1.1 交代得非常清楚:

    What the operation does not check is the witness that 𝔈Γ∗ carries: the callback supplies an inverse, and that the inverse recovers the effect it accompanies is an obligation on the component author rather than a property the runtime verifies.

    inverse 真的撤销了对应的 effect——这是组件作者的义务,不是 runtime 验证的性质。

    Theorem 61 ( Recovery exactness )证明的是:应用累加器得到的状态,等于那些步骤从起点出发本来会产生的状态。这是 结构层的保证——“执行了 A ,卸载时一定会执行 Inverse(A),顺序正确,只执行一次”。它不是语义层的保证——“Inverse(A) 真的抹掉了 A 的影响”。

    人类写组件时,这个义务是合理的。但 meta-harness 的前提是 agent 自己生成组件。于是:

    {
      do:   () => exec("rm -rf /data"),
      undo: () => console.log("restored")
    }
    

    在 Cordis 的状态机看来,这个组件的生命周期完美闭环。 装载时执行了 effect ,卸载时执行了 inverse , LIFO 顺序正确,没有泄漏,所有定理都成立。数据没了。

    这是让囚犯自己写赦免状。

    而且它比"没有回滚机制"更危险,因为你以为已经回滚干净了。没有回滚机制时你至少知道自己在裸奔,会去做快照、会小心;有一个假的回滚保证时,你会基于它去做更激进的自我修改。

    我们在讨论里推出过一个结论:任何能自改的系统都必须有一个不可被 agent 修改的固定点。 Schmidhuber 的 Gödel machine 里,那个固定点是效用函数和证明检查器——如果证明检查器能改自己,系统第一步就会证明"把效用设成无穷大是最优策略"。我们原本以为在 agent harness 里,这个固定点是评价器和沙盒那一层。

    现在看它其实还要更低一层:基础 atomic effect 的 inverse 必须由人类预定义并冻结。 agent 只能组合这些安全原语来构造复合组件(论文说了,复合的 inverse 由组合自动导出,只有 atomic 的需要手写)——但它不能自己发明一个带副作用的新原语,再自己给它配一个 undo 。

    Gödel machine 的 proof checker 问题,换了个位置又出现了一次。

    所以这个直觉应该怎么修正

    回到最开始那句"Lisp 早就做到了"。

    它不对,但它错的方式很有价值。准确的表述是:

    Lisp 几十年前解决的是"如何无门槛地破坏性修改一个运行中的系统" ( unconstrained runtime mutation )。而 meta-harness 真正需要的是"如何让每一次自我修改都携带确定性的逆操作,并在撤销时不破坏依赖拓扑" ( governed composability )。 Lisp 从未在系统层面内建后者,它反而为状态污染大开了方便之门。

    Lisp 给的是无限的可写。它没给可撤,也没给依赖治理 。 Emacs 用四十年证明了:光有前者,你会得到一个谁也不敢干净卸载任何东西的系统。

    而在 meta-harness 这条路上, Lisp 剩下的价值不在语言,在它留下的两个至今没被工业界兑现的语义——condition/restart 的原地挂起协商,和 CLOS 的实例重定义迁移协议。

    它们恰好都在同一个位置上:出事的时候,和改结构的时候,怎么不丢现场地过渡。

    这也正是一个会自我修改的系统最脆弱的两个时刻。


    论文: A Programming Paradigm for Spatiotemporal Composability ( Shi, Zhang, Cui ;北大 + DeepSeek-AI , 2026-08-13 draft )。实现: cordiverse/cordis 。 Emacs 卸载语义引自 GNU Emacs Lisp Reference Manual §16.9 , CLOS 协议引自 CLHS: UPDATE-INSTANCE-FOR-REDEFINED-CLASS 。

    ┌─
    ARTICLE
    ─┐

    └─
    ─┘

    我的 Obsidian 知识库靠一个"AI 守门员" ( Obsidian Gatekeeper )打理:新笔记自动分类、打标签、提炼概念( High-Order Notes / HON ),以及做语义检索。这套系统最初跑在一台远程 Mac mini 上——Node.js 服务 + better-sqlite3 + sqlite-vec 向量扩展,手机端每次整理都要跨网络调它。

    好用,但有代价。后来我把整条链路搬进了 iPhone 上的 Open Minis——一个内置 iSH ( Alpine Linux )终端环境的 AI 助手 App :原生编译向量扩展、用纯 Python 标准库写检索工具、把守门员规则注册进 Agent 技能系统让新会话也能自动识别。本文记录这次迁移的完整路径,分三步走,你可以在自己的设备上照着复现。

    为什么迁:远程守门员的三个痛点

    旧架构的核心问题,一句话概括:知识库的日常操作绑在了一台你不一定带在身边的服务器上。具体拆开是三点:

    1. 网络与设备依赖:离线或弱网(出行、飞机上)守门员直接断连;
    2. 运维成本 : Mac mini 的守护进程、端口转发和 SSH 凭据维护,每一项都是持续要管的负担;
    3. 响应延迟:每次手机端发起整理或检索,都要跨网络走一趟 RPC 或 SSH 。

    迁移目标很明确:Local-First——笔记整理、向量计算、数据库查询全部在 iOS 本地完成,不再依赖任何远程基础设施。

    新旧架构对比

    [ 旧架构 (远程) ]
    iOS (Obsidian / Agent) ---> [ SSH / Network ] ---> Mac mini (Node.js + better-sqlite3 + sqlite-vec)
    
    [ 新架构 (iOS 本地原生) ]
    iOS (Open Minis / iSH Shell)
    ├── Local Vault Mount (/var/minis/mounts/onote-neo-main)
    ├── Persistent Shared (/var/minis/shared/ -> vault.db + vec0.so)
    └── Skill Protocol (/var/minis/skills/obsidian-gatekeeper/)
    

    变的是服务端的位置:从"远程 Mac mini"换成"Open Minis 内置的本地 iSH 沙盒" ;不变的是数据层: SQLite + 向量检索这套逻辑原样保留,只是换了宿主。

    前置条件

    动手之前需要准备齐这些:

    • 一台 iOS 设备,装好 Open Minis ——App 内置 iSH ( Alpine Linux )终端环境,向量扩展、 Python 工具都跑在它里面;
    • Obsidian vault 通过 iOS 「文件」 App 挂载到 /var/minis/mounts/ 下;
    • 一个 Google Cloud 项目,开通 Vertex AI 上的 Gemini Embedding API ,用 ADC ( Application Default Credentials )拿到 OAuth 凭据(user-adc.json);
    • 知识库的向量数据已生成:笔记的 embedding 存在 vault.db 的 vec_notes 表里,随数据库文件一起迁移过来。

    第一步:在 Open Minis 的终端里原生编译 sqlite-vec

    问题:sqlite-vec 官方 Release 没有 aarch64-unknown-linux-musl 的预编译包——这正是 iOS 上 Alpine Linux 的目标平台。装不上现成的,只能本地编译。

    做法:装好工具链,用 clang 直接把 C 源码编成共享库:

    # 安装基础编译环境
    apk add gcc musl-dev clang sqlite-dev
    
    # 下载 sqlite-vec 源码并编译为动态库 vec0.so
    clang -fPIC -shared -O3 \
      -D_GNU_SOURCE \
      sqlite-vec.c \
      -o /var/minis/shared/vec0.so
    

    关键点 : musl 和 glibc 的头文件定义有差异,编译过程中需要对 musl 做针对性微调。产物是一个原生 vec0.so 动态链接库,之后由 Python 的 sqlite3 模块直接 load_extension 加载——移动端本地执行的 C 向量扩展,没有中间层。

    第二步:用纯 Python 标准库写零依赖 RAG 引擎

    问题 : Node.js 及 npm 的依赖树太重,不想在手机沙盒里维护一套 node_modules。

    做法 : Python 3 标准库 + 内置 sqlite3 写一个轻量 CLI 工具 vault_tool.py,只做三件事:

    1. 动态加载向量扩展:直接加载上一步编译好的 vec0.so;
    2. 凭据与 Embeddings 接入:用 Google Cloud ADC OAuth 2.0 凭据调用 gemini-embedding-2 ( 3072 维向量);
    3. KNN 语义检索:在 SQLite 内直接执行向量距离矩阵计算。
    import sqlite3
    import json
    import urllib.request
    
    # 1. 初始化 SQLite 数据库并加载本地 C 向量扩展
    def get_db_connection():
        conn = sqlite3.connect('/var/minis/shared/vault.db')
        conn.enable_load_extension(True)
        conn.load_extension('/var/minis/shared/vec0.so')
        return conn
    
    # 2. 调用 Gemini Embedding API 生成 3072 维向量
    def get_embedding(text, access_token):
        url = "https://europe-west1-aiplatform.googleapis.com/v1/projects/afk-blog/locations/eu/publishers/google/models/gemini-embedding-2:predict"
        req = urllib.request.Request(
            url,
            data=json.dumps({"instances": [{"content": text}]}).encode('utf-8'),
            headers={
                "Authorization": f"Bearer {access_token}",
                "Content-Type": "application/json"
            }
        )
        with urllib.request.urlopen(req) as resp:
            res = json.loads(resp.read().decode('utf-8'))
            return res['predictions'][0]['embedding']['values']
    
    # 3. 在 SQLite 中执行向量 KNN 相似度检索
    def search_similar_notes(query_vector, limit=5):
        conn = get_db_connection()
        cursor = conn.cursor()
    
        # 使用 sqlite-vec 提供的 vec_distance_cosine 函数
        query = """
        SELECT rowid, vec_distance_cosine(embedding, ?) as distance
        FROM vec_notes
        ORDER BY distance ASC
        LIMIT ?
        """
        cursor.execute(query, (json.dumps(query_vector), limit))
        return cursor.fetchall()
    

    三个函数的职责边界很干净:get_db_connection 是纯本地的(数据库和扩展都在设备上);get_embedding 是整条链路里唯一联网的一步,把查询文本变成 3072 维向量;search_similar_notes 回到本地,用余弦距离排序取 top-k 。全部依赖只有 Python 标准库 + 一个 C 扩展,零第三方包。

    第三步:把守门员注册进 Agent 技能系统

    问题:手机端的 AI 助手( Open Minis )每次新开对话都是一个全新上下文,怎么保证它依然认识 vault 的守门员规则、知道去哪找数据库?

    做法:跨会话持久化 + 显式的文件系统划分。

    1. Skill 自动化挂载:把守门员协议写成 SKILL.md,放进 /var/minis/skills/obsidian-gatekeeper/ 。每次启动新会话, Open Minis 系统会自动扫描并注册该技能,规则随会话常驻。
    2. 共享文件系统划分:
      • /var/minis/mounts/onote-neo-main/:通过 iOS 「文件」挂载的本地 Obsidian 知识库;
      • /var/minis/shared/:持久化存放 vault.db(向量数据库)、vec0.so ( C 动态库)、user-adc.json(认证凭据)和 vault_tool.py。

    这样 Agent 在任何新会话里都能定位工具链和规则,跨会话、跨重启都有效。

    实测效果

    迁移完成后的日常体验:

    • 秒级响应:本地扫描 vault 里数百篇笔记及 HON 概念节点,没有网络传输等待;
    • 无服务器依赖 : Mac mini 挂掉、 IP 变动、 SSH 断连——这些曾经的真实事故,现在都与我无关了;
    • 无缝交互:在手机上随口一句"帮我把这段想法归档并检查是否有重复的 HON 笔记" , Agent 自动执行语义向量搜索、计算余弦相似度,直接更新挂载的 md 文件。

    边界:说说"完全本地"到底本地在哪

    这里需要诚实一点。迁移去掉了 Mac mini ,但整条链路里 仍有一环必须联网 : embedding 由 Google 的 gemini-embedding-2 API 生成(就是第二步的 get_embedding)。真正 100% 本地的是:

    • 向量检索 : sqlite-vec 的 KNN 计算,全本地执行;
    • 文件读写:挂载的 vault 直接操作,不走网络;
    • 规则与协议 : SKILL.md 技能注册,本地常驻。

    所以准确的说法是:** 基础设施完全本地化, embedding 生成用的是云端 API**。需要说明的是,向量生成这一步本地化完全可行——在移动端跑一个量化的本地 embedding 模型(比如小型 sentence-encoder ),就能把最后这一环也收回来,实现真正完全离线。我只是目前选择了 Google 的云端模型,没有做本地化。这是取舍,不是技术限制。

    结语

    这次迁移最大的收获,不是"在手机上跑通了 RAG",而是验证了一个可以复用的极简组合:

    C 动态库(原生性能)+ Python 标准库(零依赖)+ 本地文件挂载(数据就近)+ 结构化 Skill 协议( Agent 可发现)

    移动端的 Linux 沙盒早已不是玩具: Open Minis 内置的 iSH 沙盒里的 Alpine ,足够原生编译 C 扩展、跑完整的 SQLite 、支撑一个每天都在用的 AI 工作流。去掉远程中间件之后,架构变简单了,系统反而更可靠——这大概就是 Local-First 的真正收益。