Last month's Contributor spotlight interview I mentioned honk, the native Hoon compiler I wrote for Nockchain and talked about why I built it. This post is intended as a follow on to describe the how: what honk does differently from the compiler it replaced, where the twenty-fold speedup actually came from, and keeping sure work stayed correct as performance improved. It gets relatively detailed, so be forewarned. While I won't provide a TL;DR: explicitly, I have tried to frontload the core takeaways.

As those familiar with Urbit development will know, Nock is a tiny instruction set over nouns, where a noun is either an unsigned integer or a pair of nouns, and Hoon is the most prominent language that compiles to it. The Hoon compiler is itself written in Hoon, as the ++ut core in hoon.hoon, and it is a compiler in the most literal sense: it takes a noun for the subject type and a noun for the parsed expression, infers a type, and emits a Nock formula, and every one of those things is a noun. Until honk, Nockchain built its kernels with hoonc, a [NockApp](TK nockapp repo link?) that loads the compiled ++ut and runs it as Nock on [NockVM](TK nockvm repo link), the Rust interpreter the rest of the system runs on. hoonc is the same compiler Urbit uses, but repackaged to be CLI-and-CI-friendly, maintaining the virtue that the compiler is defined by exactly the semantics it compiles. But it's also why a clean build of the roswell kernel took over ten minutes.

honk replaces that pipeline with native code, in three pieces. hatch is a Rust parser for Hoon, written as chumsky parser combinators with no separate lexer, that produces a typed syntax tree with source positions attached. I am not the original author of hatch. The originator seems to value their privacy, so I won't identify them, but they did incredible work getting the first ~80% of hatch done and their work is what made honk possible to begin with. honk is approximately a Rust reimplementation of ++ut, ported arm by arm. It's wrapped in a build driver that resolves imports, embeds the compiled hoon-138 prelude and jet state, so that nothing has to bootstrap compiles. honk writes JAM artifacts to disk just as hoonc does. The third piece is nockasm, ~lagrev-nocfep's legible notation for Nock. I contributed the Rust implementation to nockasm so that I could migrate honk from emitting Nouns to emitting nockasm. Apart from speed, this also made persistent incremental compilation much more tractable and made compilation artifacts much more auditable. nockasm's Rust implementation represents a noun as a DAG with its sharing preserved. honk's persistent build cache stores its products in that format, which is why a type subgraph shared by dozens of build products is written to disk once, and it is also what I reach for to diff two compilers' artifacts when they disagree. Diffing jams when debugging honk during the initial drive to parity was…unpleasant and required a lot of iteration on tools for legibilizing jammed nouns. Most of the legibility priority there was agentic rather than human, but being human-friendly was beneficial in it's own right.

The rewrite helped massively in running Nockchain node kernel workloads. The following specs are benchmarked on an Apple M5 Max, using the median of three runs:

The last row is not a typo. honk spends memory to buy time and I make no bones about that. A later section explains where the memory goes and I will suggest what might be required to get it back. The in-development honk-lsp often uses less memory than honk's peak RSS.

I had one rule governing my effort on honk: the output must be byte-for-byte identical to hoonc's. Not structurally equivalent. Not equal once the debugging metadata is normalized away. The same bytes. And it needed to be for all six production kernels and for the compiler's own source. If an optimization didn't support the byte-for-byte target, it wouldn't fly because this is the reason the conformance and performance work could move quickly.

What honk is not, and what is next

honk is not an Urbit compiler, and I want to be precise about why so nobody reads this post as a claim that it is. It targets Nockchain's pinned hoon-138 environment. It has no %ford, no %clay, no desks, marks, or kelvins, and it does nothing for the runtime side of an Urbit ship; Ames and Gall run exactly as fast as they did yesterday. What it is, is a native implementation of ++ut that produces the same bytes as the Hoon one for every program we have, and that is the part an 'Urbit compatibility mode' would build on. I would like to build that mode and that I can't do it well without the people who maintain the rest of the stack. That is still true, but someone else would need to step up and do a lot of the legwork. Let me know if you are interested.

Aside from the compatibility stuff, the open items to get it from where it is to where it needs to be are easily stated:

• The Roswell kernel compiles in 63.7 seconds on an M5 Max against a 60-second gate I set for it, so the gate is a near miss rather than a pass, and the profile ranks noun and value transport first and map and cache growth second.
• Cold-build memory is 4.1 GiB where hoonc needs 1.2, and I have not tried to close that gap yet. The two levers I have not pulled are compiling independent files of the import graph in parallel and emitting nockasm node tables directly instead of building nouns and lifting them.
• And the three native caches from the correctness section still identify a gene by a 64-bit signature without confirming the hit.

The thing I am spending my time on now is editor tooling, because a compiler that finishes in seconds changes what an editor can do. honk-lsp runs the real compiler on a dedicated thread with open buffers as versioned overlays over the filesystem, so an unsaved edit is checked against the same engine that builds the kernel, through an artifact-free check that parses, resolves imports, and type-checks without evaluating or jamming anything. On top of that sit diagnostics for unsaved buffers, symbols, hover with inferred types once a check lands, go-to-definition that follows compiler-resolved arms and imports with a structural fallback, references, safe rename, completion with provenance, and reference-count and signature code lenses. It has its own performance harness, separate from the build benchmarks, because the latencies that matter in an editor are different ones.

In the spotlight I also mentioned carrying over the lessons from honk into the next compiler. I did. I wrote a Rust compiler for ~lagrev-nocfep's Jock language using his spec implementation in Hoon as the parity anchor. It took one night, a little under 12 hours, to hit parity. When I did, it was 20x-50x faster than the original spec compiler which was written with some consideration for runtime efficiency. This was possible in large part to ~lagrev-nocfep's very thoughtful design of the grammar, compile-time semantics, and runtime semantics. It was also possible because I had honk to anchor on as a compiler implementation design "true north." The Rust compiler is named jonk. I let an agent pick the name and found it too funny to override.

Ok, let's dive into the details about honk and how it came to be. You can also throw the link to this post to an agent and have an interactive discussion with it, if that's more your speed these days.

Why hoonc was slow, and why the fix was a rewrite rather than a tune

hoonc is a NockApp originally named choo. The NockApp carries a cached compiled prelude, a build cache, and a parse cache, and its %build cause runs ++ut over an entry file and its imports and hands back a jammed artifact. It has separate caches for parses and builds. It has a pre-warmed bootstrap state with the compiled Hoon prelude already injected because I got impatient with Bazel builds losing ~3 minutes on compiling the prelude every time. The Bazel builds are nominally stateless because there's not a clean way to merge/reconcile the jammed checkpoints from the NockApp. I did experiment with incremental builds in Bazel and got it working, but there were countervailing factors that made it too slow to bother with. Mostly because merges of large nouns (the checkpointed state jams) are slow and there's nothing I can do about that. At the time the persistent memory arena (PMA) didn't exist, but it doesn't materially change anything for this.

Everything hoonc's prelude compiler touches on the way is a noun: the subject type, the parsed expression, every intermediate type that inference produces, the emitted formula, and the key of every cache. A type comparison is a tree walk. A cache lookup mugs a noun and then compares nouns on a hit. Checking whether two cores are the same core is a walk over their batteries. NockVM does have the standard memoization jets (same as Urbit/Vere) for the important ++ut arms. It's worth being precise about what those jets do because the word "jet" suggests native code. mint, nest, mull, crop, fuse, fish, redo, and rest are all registered, but each one builds a key from the subject type, the argument, and the battery, looks it up in the interpreter's memo table, and on a miss runs the Hoon. They are caches in front of interpreted code. This is exactly what they are in Vere too. These jets aren't optional. You will vaporize the Mariana Trench before anything finishes compiling without the memo jets.

NockVM's equality jet is unifying: when it proves two nouns equal, it rewrites one to point at the other, so the next comparison of that pair is a pointer check. In a long-running compiler process that side effect quietly turns a great many tree walks into word compares. This comes back when I discuss correctness. A jet that had been leaning on that side effect went wrong the moment honk handed it nouns that never unify.

As I mentioned in the spotlight, there were a few rounds of tuning that I did. The first round was the build graph: Bazel, warm caches, and low churn brought end-to-end hoonc builds on the happy path from an hour and a half down to three and a half minutes. The second round was NockVM itself, and the largest piece of that was the PMA, which let a NockApp carrying an Arvo subject of more than 16 GiB run at a peak RSS of around 1.5 GiB. I did optimization work on NockVM prior to the PMA that sped it up by 2-2.5x but unfortunately some of that efficiency gain got traded off for the PMA's pointer arithmetic overhead. In my testing, Vere is about 2-2.5x faster compiling its prelude versus hoonc + NockVM compiling hoon-138. NockVM is still a tree-walking interpreter, not a bytecode VM, so we hope to close the gap when we have time to pursue to that effort. The newer prelude Vere compiles is somewhat simpler than hoon-138, but I don't think it materially changes the ratio. I inflicted similar rounds of optimization on hoonc as well: a reorganization with better build and parse caching, a longer checkpoint interval, a pre-booted bootstrap image so a fresh hoonc doesn't rebuild its own state on every start, and faster checkpoints after that. While each helped eek out performance improvements, none of them changed what a compile fundamentally is under hoonc: an interpreter walking nouns.

Here is the ceiling argument as I saw it: Once the build graph is cached and the interpreter's memory is under control, what's left is the cost of the compiler's own data structures, and that cost is fixed by their representation. A type built as a noun has no way to share structure with an equal type built a moment earlier, because nothing at construction time knows they are equal; that's what hash-consing is for, and nouns don't have it. Two equal types that haven't been unified cost a full walk to prove equal. Memoization is keyed by nouns, so every lookup pays a mug and a compare before it can hit. The interpreter loop sits between each of these operations and the CPU. You can make any of them a constant factor faster and I did. You cannot move them into a different complexity class without changing what the compiler operates on. I said in the interview that the next step for NockVM is probably a bytecode VM, and I still think so, but even that leaves aside the data structures. If I wanted a compiler that was faster by an order of magnitude rather than by a percentage, it had to be native.

"Native" meant something specific at the start, and less than it means now. hatch parses the source into a Rust syntax tree. honk resolves the /= imports itself, walking the dependency directory and refusing cycles. It embeds the compiled hoon-138 prelude as a hoonc-built formula and type, a little over a megabyte between them, along with the cold jet state, so a compile starts from a ready subject instead of booting a compiler. honk gets parity tested on hoon-138, so it can compile it, I just don't want to inflict that cost on end-users unnecessarily. honk was designed with both casual use and integration into Bazel builds in mind. honk compiles each entry through a Rust port of ++ut and writes the artifact hoonc would have written. What "native" did not mean, at first, was native data. The first honk represented types and formulas exactly as hoonc does, as nouns in a slab, because that was the shortest path to byte-for-byte parity, and even then was 2-4x faster than hoonc. Getting rid of the noun-structured-and-addressed intermediate representations in the honk compiler is how I drove it from being ~4x faster on cold builds to ~20x.

++ut is about 2,800 lines of Hoon, but the Rust that implements it is close to fifteen thousand lines in one module, and more than a hundred places in that module cite the Hoon they implement. The code is very well commented; if you want to check whether honk's find does what hoon-138's ++find does, the Rust tells you exactly where to look. This was, again, secondary to parity-checking the compilation artifacts themselves but it was a later development that has made code review and fixing compilation disparities less burdensome.

Parity first: the oracle that made the rest possible

I decided early that I would prioritize correctness for honk and that "correct" would have exactly one definition: the jam bytes hoonc writes. Naturally, some consideration of "fast" was required to ensure I had the ability to compare output artifacts before the heat death of the universe. The native compiler landed in July 2026 with byte-for-byte parity with hoonc on all six production kernels and on hoon-138 itself, and somewhere between two and four times faster on cold builds. At time of writing in the honk-lsp branch, hatch is ~26k LoC of Rust, honk is ~34k LoC of Rust, and honk-lsp is 9k LoC of Rust.

Byte-for-byte is stricter than it sounds because a jammed compiler artifact carries more than executable code in the form of a Nock noun. When the source is compiled with debugging on, every %dbug node in the syntax tree becomes a %spot hint in the emitted Nock: a file path, a start line and column, an end line and column. Those hints are bytes in the kernel. So hatch has to produce the same spans ++vast does, down to the rule that expands a rune's span backward over the doc-comment block above it in some positions and not in others. These little nits happen all over the place. The standard kernel artifact is not the bare compiled program. It is that program wrapped by a handful of gates that hoonc defines in its own source, gates that inject the directory hash, box the result as a trap vase, and so on, and those wrapper gates carry %spot hints too, pointing at specific lines of hoonc.hoon. honk reproduces them by compiling the same wrapper text padded with the right number of leading newlines so the spots come out at the same coordinates, and a wrapper-asset parity test compares eleven of those batteries against the ones hoonc produces. Where possible, I made principled fixes to the parser in order to align it with the original. It wasn't always possible. If that sounds like an absurd thing to have to get right, it is. Hoon's grammar is a blasphemous outrage (I apologize for nothing, Urbit devs, so don't ask). Much of the final parity work on honk was dealing with the long-tail of %spot hints not matching on the column and line values.

CI compiles each of the six kernels with both compilers, cold, and runs cmp. It compiles 55 type-checking probes with both compilers. The probes are small self-contained files that pin inferred types with !> across auras, forks, wet gates, core variance, casts, and folds, each pair compared byte for byte with an empty dependency directory so both sides see the same tree. It compiles hoon-138 itself through honk's native path with the embedded prelude switched off and compares the result against hoonc --arbitrary; that job peaks around 14 GB of RSS, so I decided to ensure it runs alone. Underneath the CI are the unit suites: 239 tests in honk across the library, CLI, mint, and rejection suites, 278 in hatch, and 183 in NockVM. All of the artifact gates are cmp. None of them knows anything about a particular kernel. The self-mint gate was the last of these to close; I'll explain why later.

An efficient correctness oracle is a huge source of leverage for everything else. Without that, "is this optimization correct?" is a expensive judgment call. Change the compiler, build six kernels, run cmp. If the bytes match, the change did not alter the compiler's observable behavior on the largest programs we have, or on the compiler's own source. If they don't, the diff tool points at the first differing axis and you go look. This also meant I ditched many ideas that were byte-correct but slower. The early work on the oracle bought the ability to make aggressive representation changes to a type checker, week after week, without accumulating a mountain of assumptions backed by "I thought this was equivalent when I did it."

Getting there was a grind. A parity failure on a kernel doesn't come with a message. Rather, you get two twenty-megabyte jams whose bytes diverge at some offset. The tooling that fell out of that period is a structural diff that cues both artifacts and walks them to the first differing leaf, a mode that locates every %spot hint referencing a given file and line so you can see what each compiler thought a rune's span was, an axis extractor to pull one subtree out for closer inspection, and later nockasm text so the subtree was human-legible. The jam-diff utility eventually fell out of these efforts to make disparity investigations tractable. The flag that lets you ignore the non-semantic Nock opcodes comes from when the compiler was still materially broken and incomplete.

The wall: native self-mint of the prelude would not finish

The application-specific kernels were compiling with parity but I couldn't build the Hoon prelude in a reasonable amount of time and it had continually climbing RSS over time. As a personal aside, of all the work on honk, I think this was the most interesting stretch.

The Hoon prelude is probably the most annoying and difficult thing to get compiling correctly as a Hoon compiler author. The prelude seems like it's designed to incrementally bootstrap Hoon language functionality just so it can show off the backflips and pirouettes it'll make your compiler perform on command. This is another reason for the cached prelude bootstrap: it enabled working on the simpler application-specific kernels and getting them to parity before I finished getting the prelude compiling in honk with full parity. At the time I'm speaking of, every kernel built fine because every kernel compiled against the embedded prelude. If you switched the embedded prelude off and asked honk to mint the standard library from source it would never finish. I reproduced it in mid-June on a machine with 128 GB of RAM: 2.9 GB resident ten seconds in, 42.5 GB at ten minutes, growing at about 4 GB a minute in a straight line with no plateau, still inside the compile phase, on course to exhaust the box in half an hour to fifty minutes. I had a run simply get OOM-killed after forty-nine minutes. You could say at that point I had a native compiler for everything except the compiler. Not good enough.

In spite of the performative backflips of Hoon bootstrapping, the prelude-shaped wall I Wile E. Coyote'd into didn't exist for no reason at all... First, the compiler's slab was a grow-only bump allocator that I had deliberately leaked so its nouns would live for the whole process. The prelude was minted in one monolithic call. Resident memory was cumulative allocation. Second, nothing interned types properly. Every constructor allocated a structurally equal type at a fresh address. This defeated the pointer short-circuit in noun equality and turned every mug-keyed and address-keyed cache into a miss. So the runtime half of the problem was super-linear deep walks and the memory half was permanent duplicate bytes. Third, subject deepening: when ++ut compiles a core it embeds the entire current subject type as that core's context, so resolving a name walks a spine that grows with every arm compiled before it. This is is quadratic over the roughly ~530 arms of the prelude. hoon-138's cumulative six-layer subject is the worst case I've been able to find so far. Behind those were smaller amplifiers: a redundant full-prelude play worth about five seconds, the recursive molds and some 193 wet gates that hit the heaviest paths hardest, and lazy arm resolvers that were never cleared because cached types held references to them by id. I wrote at the time that the keystone fix was interning at the type constructors.

The first false start was chunking. The prelude is a => chain of layers, so I built a checkpoint-and-rewind primitive for the slab and a driver that minted each layer in a fresh compiler and carried only the resulting type forward. It reclaimed six of the seven layers, about 4 GB through them, and then hit the seventh, which is the standard library proper, one giant core that mints as a single call and climbed past 23 GB on its own. Chunking within that core, arm by arm, was measured and ruled out: arms in ++ut reference each other so densely that minting any one arm re-plays a large fraction of the core's types through the lazy resolvers, so per-arm reclamation neither bounds the peak nor avoids heavy recompute.

The second false start was a frame arena. The canonical Vere shape: per-arm scratch allocated in a frame and reclaimed at frame pop while the shared core type stays live. It worked as intended. Once types had been flipped to native handles, per-arm scratch turned out to be the dominant growth on the node kernel, and the frame arena brought that compile from over 900 seconds at 61 GB to 153 seconds at 10 GB. The RSS burden that remained was not scratch, it was preserved, shared, un-interned structure, and no amount of reclaiming what you are about to discard helps with what you have to keep. Worse, reclamation made every address-keyed cache in the compiler a dangling-pointer hazard, which was the exact bug class the rewrite was supposed to remove. I retired the frame arena within a week. My recommendation to myself on June 15 was to ship the hybrid, embedded prelude and all, and to treat self-hosting as gated on a representation change rather than on any amount of memory management. A lesson for the reader: If you meet a Noun on the road to efficiency, kill it. Nothing in software is sacred to me except correctness and speed.

My plan for the representation change: native Rust Type and Formula values with sharing and hash-consing as the working representation, nouns emitted only at named boundaries, with five goals: bound the self-mint, get faster, stay byte-exact at every step, eliminate the noun-representation bug class, and exhaustively match over a small normalizing type algebra instead of twelve thousand lines of string-tag dispatch on noun shapes. I red-teamed this against the code before kicking off the native IR effort. The review produced eighteen findings, seventeen confirmed and one mostly confirmed, and its verdict was that the direction was probably right but the plan was not yet safe to execute. The plan overstated how ready the oracle was, understated how many places nouns still cross a boundary, and made byte-exactness depend on things that were underspecified. The bar the review set became the bar for the whole migration. Every "native representation makes this go away" claim must become an ownership invariant, a byte-exact fixture, a cache/lifetime matrix entry, or an explicitly named boundary. The acceptance criteria that fell out of this were strict cmp on every kernel with no tolerance, a self-mint that completes with bounded memory backed by ownership accounting rather than a lucky peak number, the Roswell kernel under sixty seconds against a recorded baseline, and the noun ++ut retired.

Two of the findings generalize well beyond this compiler. The first is that a bare Noun inside a native data structure is an alien pointer. A noun is only meaningful relative to the arena that owns it, and the release build skips range validation on the fast path, so a quoted constant or a hint clue stored as a raw noun leaf in a native formula could point into a parser stack, an evaluator slab, or a frame that has already been popped, and would resolve silently to the wrong memory rather than fail. The plan had sketched exactly that. The fix was a provenanced leaf type, a small atom inline or owned bytes otherwise, and a checked copy at every materialization into a destination slab. The second finding is the one I had half-believed and needed to stop believing: reference counting plus hash-consing plus destructors does not by itself solve a memory wall. It removes the dominant sources, the duplicated types and the quadratic subject, but a compile also retains evaluator contexts, wrapper products, fold results, and cache entries, and none of those go away because the type representation changed. Keeping allocation under control needs an explicit ownership and lifetime design, and this carried into my acceptance criterion to require "ownership accounting" and not just "under some number of gigabytes". The third finding was that caches need a semantic migration matrix and not a promise to delete or shrink them. This comes up again when we discuss where the tension between speed and correctness lives most concretely.

The process shaped the result, and the process was heavily shaped by the way I like to use coding agents. I ran the search for the fix as a contest. Ten independent agents, each in an isolated worktree with a fresh context. Each agent was assigned one angle and all were held to an acceptance contract that I wrote down before any started: mint hoon-138 through the native path, match hoonc --arbitrary byte for byte, keep memory bounded rather than linear, finish in about a minute, and do it without waivers, re-jam normalization, fixture-specific bypasses, or deleted metadata. The contract mattered more than the parallelism. I didn't just take a winning branch from this and merge it wholesale but it did give me a much sharper picture of where the allocation burden resided and which invariants the caches depended on.

The arena migration, one representation at a time

We'll go through this in details subsections, as the details are what made this work possible. Each subsection covers: what was represented as nouns, what it became, the measured result, and the variant that was rejected. Measurements are release-LTO builds on my 9985WX workstation, pinned to one CPU, with adjacent control brackets and SHA-256 equality on every output. Throughput gain is control midpoint divided by candidate minus one.

Types: a hash-cons table with dense ids

• TypeTable interns children before parents, shallow-hashes canonical child ids, confirms collisions with exact shallow equality, and hands back the existing handle for a structurally identical node. Equality of two types becomes one word compare. Sources: intern.rs, TypeTable and intern_shallow; ty.rs, TypeId and TypeRef.
• The "atomic flip": producers were flipped one connected step at a time from returning noun types to returning native types, with boundary conversions bridging the not-yet-flipped callers, so the tree compiled at every step and the native region grew monotonically. Source: ATOMIC-FLIP-TRACKER.md, strategy.
• The handle representation: TypeRef is one non-null pointer into a context-owned boxed slot carrying a TypeId(u32). Clone is a word copy, drop is a no-op, caches key on the u32. Measured +1.57% Wallet, +3.14% Roswell, +1.72% Dumbnet over the arena-Hoon parent. Sources: ARENA-TYPE-IR.md, performance result and rejected variants.
• Rejected: swapping the interner's DefaultHasher for the byte-wise FastHasher was byte-exact and 9.02% slower on Wallet, because carried leaf hashes write byte slices. Reverted. A good example of a "faster hash" being slower.
• Forks: %fork members became native DAG children, but the original mug-ordered treap is retained as the serialization witness so typed output still emits the exact Hoon set shape. The adaptive detail: first traversal uses inline storage, second traversal promotes to a cached slice, so one-shot forks never retain an allocation. Sources: NATIVE-TYPE-DAG.md, design and performance experiments.

The Hoon AST: a sidecar DAG, then an arena

• Stage one gave every node of the borrowed parser AST a scope-bound identity, computed spot-sensitive structural signatures compositionally in one traversal (Sig64), and materialized each node's canonical noun at most once per scope. Dumbnet +1.66%, Wallet +6.15%, Roswell +11.36%. Sources: NATIVE-HOON-AST-DAG.md, release-build performance and rejected variants.
• The rejected first version is the lesson: retaining cloned AST nodes including compiler-generated temporaries regressed Dumbnet from 83.72 s to 104.79 s and doubled peak memory to 20.67 GB. Identity-only without noun reuse was also worse. One-time materialization was the essential half.
• Stage two replaced the pointer-keyed sidecar tables with a dense HoonId(u32) arena in post-order, and treated compiler-generated lowerings as short nested LIFO scopes instead of an unbounded cache. HoonId(u32) is not a mug hash wrapper, it's a dense index. Roswell +7.65%, peak RSS down 8 to 11%. Sources: ARENA-HOON-IR.md, release-build performance, rejected variants, and lifetime and unwind safety.
• Rejected variants that read like a lab notebook: generic child edges in a per-node hash map (-1.97%), a hash-free traversal stack (-0.50%), and direct recursion for additional rune forms that measured inside noise. Only the two measured-hot binary forms kept direct id edges.
• The unwind-safety detail: HoonAstScope restores the previous arena in Drop, including during panic unwinding, so no stale address survives a caught error. This will be addressed again later.

5.3 Formulas: a hash-consed DAG that stays a DAG until output

• Generated Nock is carried as FormulaId(u32) in a compile-local FormulaArena, with the historical cons, comb, cond, flip, flan, flor simplifications implemented over ids in the same check order. Materialization to nouns happens only at explicit formula-as-data boundaries (++musk evaluation, hint clues, batteries, %zpts) and at the final output, emitting each distinct node once. Sources: ARENA-FORMULA-IR.md, representation, semantic boundaries, and performance evidence; formula_dag.rs, FormulaNode and FormulaArena and materialize.
• Axes are u64 when they fit and BigUint otherwise, because honk once had a 64-bit axis ceiling and that was a semantic bug, not a limitation.
• Measured about +2.0% and, more importantly, formulas vanished from the profile: interning was 0.157% inclusive. The remaining profile was noun equality and type tables, which set up the next step.

Seminouns: where the real time was hiding

A seminoun is a noun with holes in it. Concretely it is a pair of an ordinary data noun and a stencil, a mask over the noun's shape that says which subtrees are actually known: a %full stencil with no blocks means the whole subtree is a real value, a %full stencil with blocks means it is unknown, and a %half stencil splits into a left and a right stencil so knowledge can run out at any depth. The compiler carries them in two places. Every %core type holds one in its coil, because at compile time a core's battery is known, it is literally the formulas being generated, while its payload generally is not, so the type records "battery known, payload blocked". And ++musk is an interpreter for Nock over seminouns: it runs a formula against a partially known subject, following the opcodes as far as the known parts allow and stopping the moment a computation touches a hole.

That interpreter is how constant folding works. ++bran projects the current subject type into a seminoun, constant atoms are known, cells combine, cores contribute their battery, forks and %noun are blocked, and %hold is unrolled under a cycle guard. ^~ then mints the expression, projects the subject, and runs ++musk on the result. If the answer comes back fully known, the emitted code is replaced with the constant [1 noun]; if evaluation stopped or is waiting on a hole, the code stays code. Bunts go through the same door, which is why a mold's bunt lands in an artifact as a constant rather than as a formula. honk keeps the same lattice natively, with one addition for batteries that are still being compiled: a lazy state that resolves arm by arm on demand, which is the seam the arena work in this section had to make exact.

• Background for Urbit devs: ++musk is the abstract Nock interpreter in hoon.hoon that evaluates formulas over partially known subjects (seminouns with stencil masks) to constant-fold ^~ / %ktsg and to resolve arms during find. honk reimplements it natively and also keeps a NockVM context for concrete mack evaluation. Sources: hoon-138.hoon, +$seminoun and +$stencil and ++musk; ut/mod.rs, blow_ktsg.
• The problem: seminouns rebuilt structurally equal cores at fresh slab addresses, so raw-pointer caches missed and fell back to full structural noun comparison. Before the fix noun_eq was 56.17% of inclusive samples.
• ValueArena assigns one ValueId to structurally equal complete nouns, canonicalizing direct atoms by value and cells by child ids. SemiArena hash-conses the four seminoun states (complete, blocked, half, lazy). Musk memo keys become exact identities instead of hashes. Sources: value_dag.rs, ValueId and ValueArena and import; semi_dag.rs, SemiNode and SemiArena; ARENA-SEMINOUN-IR.md, representation and invariants.
• The result, in two isolated commits: value identity alone took Dumbnet from 80.77 s to 43.38 s (+86%), and moving the full lattice to ids took it to 31.07 s (a further +40%). Final balanced gate 83.97 s to 31.48 s, 2.668× throughput. noun_eq fell to 3.02% self. Source: ARENA-SEMINOUN-IR.md, performance evidence.
• The lesson to state plainly: three careful arena migrations bought roughly 10 to 15% combined, and the fourth bought 2.7×. The profile said where the time was but the big win came from hitting the right part of the architecture.

The post-arena frontier and the discipline of small wins

• Canonicalizing live type leaves by mug bucket with exact collision checks (+1.34% Dumbnet, +1.50% Roswell) and resolving a compared cell's head and tail in one pointer resolution inside noun_eq (+2.42%, +2.17%). Sources: POST-ARENA-PERFORMANCE-FRONTIER.md, accepted changes and rejected variants.
• Rejected, with numbers: pruning discarded type-algebra results (-0.64%, -1.62%), inline u64 axes in the type path (-1.86% despite saving 49 MB), caching Spot signatures (positive alone, negative combined with canonical leaves, preserved in a worktree for a future PGO regime), inlining NounSpace::empty targeting 635 million calls (-0.7%), and widening the paired cell read to hotter callers (-1.04%, -2.06%).
• The point: the accepted set is not the union of everything that was individually positive. Interactions with optimized code layout are real and were measured rather than assumed.

The serialization diet and the persistent cache (PR #153)

• Incremental builds: a content-addressed cache of per-file products stored as multi-root nockasm DAG packs, keyed by blake3 merkles over source, import closure, and a compiler fingerprint, so a compiler change invalidates cleanly and a source edit rebuilds only its reverse dependency closure. Sources: PR #153; build_cache.rs, BuildCache and read.
• Why nockasm: the sharing-preserving DAG serializes the big shared type and trap subgraphs once instead of once per entry. The benchmark makes the case: the boxed-tree lift of the 19 MiB Dumbnet kernel was killed after 175 s at about 52 GiB RSS, while the DAG AST conversion takes 813 ms p50. Sources: performance.md, kernel serialization benchmark and reference result.
• The first cut of the cache round-tripped every noun through jam and cue just to change Rust types, and re-serialized packs to prove canonicality. Profiles said that was most of warm-start time. The fixes: SlabToNockasm lifts slab nouns straight into hash-consed nockasm nouns with parents keyed on child intern ids, reads hydrate only the requested root, cold state decodes in place instead of deep-copying every battery twice per run, and NockJammer::jam got a word-at-a-time writer with an open-addressed backref memo that is byte-identical and about 5× faster. Sources: nasm_bridge.rs, module notes and convert; performance.md, serialization bridges.
• Numbers against the first cut on the same host: cold 28.8 s to 19.5 s, warm no-op 4.8 s to 1.0 s, peak RSS down 26 to 63% depending on scenario. Under Bazel: 20.2 s cold, 1.3 s seeded no-op, 3.1 s seeded root edit, seeded and unseeded jams byte-identical.
• Last-mile items that belong here: jemalloc in the compiler binary (the system allocator was about 25% of cold-build samples), pooled compile-scope arenas, one getcwd per process instead of per %dbug node, and Sig64 mixing one splitmix64 round per word instead of eight FNV rounds.
• Chunked prelude mint: the canonical prelude is a chain of six layer cores, and minting each layer in its own fresh Ut and slab bounds peak memory to one layer plus the carried subject. This is what made native self-mint of hoon-138 complete at all. Source: PHASE0-CHUNKED-DECISION.md, executive summary.
• PGO: a whole-graph profile-guided build trained on Wallet and Dumbnet, with a built-in check that the optimized compiler's Dumbnet artifact is byte-identical to the instrumented one. Note the honest caveat from the records that Dumbnet is sensitive to profile-driven code layout and one arena stage measured slightly negative under PGO while positive in the source-level bracket. Sources: build-honk-pgo.sh, byte-identical verification; ARENA-HOON-IR.md, whole-graph PGO.

What this teaches about performant compiler design

None of what follows is specific to Hoon. These are the rules I would carry into the next compiler, each with a pointer to where honk paid for it. And I did. More on that at the end.

Identity is the whole game. If two equal things can be made to have one identity, then equality is a word compare, memo keys are exact, and no subtree is ever hashed twice. The way to get there is to intern bottom-up: canonicalize children first, so a parent's identity is a function of its child ids and interning a node costs the same whether it is three nodes deep or three thousand. Where a key has to be a hash rather than an identity, confirm the hit against the stored input; a bucket with an exact compare costs almost nothing and turns a probabilistic cache into a deterministic one. Prefer dense integer ids over pointers and reference counts. A u32 index is a smaller key than a pointer, it costs nothing to copy or drop, and assigning ids in post-order puts a node's metadata next to its children's in memory. The reference-count traffic that Rc adds to recursive type algebra is real: the one-word arena handle with no destructor was worth 1.5 to 3 percent on its own, before any cache got a cheaper key.

Scope arenas to the computation that owns them, and make the discipline mechanical. An arena that lives exactly as long as its computation needs no generation counters and no reclamation logic, but only if nothing can escape it. Make the nesting LIFO, restore the parent scope in Drop so a panic cannot leave a stale pointer behind, and store copied signatures rather than scope-local ids in anything longer-lived. An arena whose ids can leak is a use-after-free with extra steps.

Every representation boundary is a cost center. Count the times a value changes representation on the hot path, then make each crossing explicit, one-way where possible, and memoized. The first cut of honk's cache serialized every product to bytes and parsed them back purely to change Rust types, and that round trip was most of warm-start time. Formulas that stay a DAG until the final emit are the same rule applied inside the compiler.

The abstract interpreter is part of the compiler. Constant folding, bunts, and lazy arm resolution all run through ++musk, and it ran on a data representation nobody had optimized because it wasn't the part of the compiler anyone thought of as the compiler. That was the 2.7×. If a compiler evaluates its own output at compile time, the evaluator's values need the same identity discipline as its types.

Caches are accelerators, never semantics. A hit and a miss must be observationally identical. That means a cache key carries every piece of context that can change the answer, which for honk is the vetting flag, the active %hold scope, and the recursive-arm state, and it means you can disable every cache and get the same bytes. The stale-hit bugs in the correctness section are what happens when a key is one field short.

Measure like an adversary would. One pinned CPU, control runs bracketing every candidate in both orders, byte-exact output checked on every run, and a stated formula for the gain. Reject changes that are byte-correct but lose throughput, and expect individually positive changes not to compose: the accepted set in 5.5 is smaller than the union of what won alone, because optimized code layout is a shared resource and two good ideas can fight over it.

Profile after every structural change, because the frontier moves. Formulas were a visible cost until the formula arena landed, and then they were 0.16 percent of samples and noun equality was 56. Each representation change re-ranks what is hot, so the profile that justified the last change is worthless for choosing the next one.

Allocator, PGO, and hashing are last-mile, not first. jemalloc, profile-guided layout, and a faster mixer were worth a few percent each once the representations were right, and would have been noise before. I would go further: a large PGO yield is a sign the source still has structural work left, because layout is compensating for something the code should not be doing in the first place.

Incremental compilation is a hashing and serialization problem before it is a dependency-tracking problem. Content-address every product by a hash over its source, its import closure, and the compiler's own fingerprint, so invalidation is a property of the key rather than a graph walk you have to get right, and store products in a format that preserves sharing, so a subgraph that dozens of entries share is written once. The dependency graph is the easy part.

Correctness versus speed

Yes, there is tension, and I felt it in three specific places. I have spent more than half my 16-year career in Haskell and Rust, I wrote a book about the former, and the reflex those languages give you is to make the type system carry the invariants so that a reviewer doesn't have to. honk is full of things that reflex rejects: raw pointers into arenas, memo tables keyed by memory addresses, an allocator that is leaked on purpose, and 156 unsafe blocks. I include detailed references in this section for those finding themselves curious about the deepest details.

The first place was the handles. TypeRef is a non-null pointer into an arena slot with no lifetime parameter. Threading one through fifteen thousand lines of recursive type algebra was the cost the arena migration existed to avoid. Eighty-seven places use a noun's slab address as its identity. The compiler slab is leaked so those addresses stay valid for the whole process. A Haskeller reads that and reaches for ST and a rank-2 type to make escape impossible, and Rust can express the same thing, but not without the borrow checker touching every function in the engine. What I did instead was write each invariant down and enforce it mechanically where I could. Every handle's lifetime is bounded by one owning Context that outlives every cache able to dereference it, and the one method that could have broken that, Context::reset, was removed in review rather than documented as dangerous. Address-keyed memos are sound only because the compile slab never recycles an address, and that sentence sits at the memo. Arena scopes restore their parent in Drop, including during a panic unwind, so a caught error cannot leave a stale address behind. Noun leaves inside native formulas carry their provenance instead of a bare pointer, which was the red team's RT-04. These aren't proofs, but they do offer us an invariant, a guard, and a regression test for each place the borrow checker could not follow, which is the shape most real systems code takes. Sources: ty.rs, TypeId and TypeRef; POST-REBASE-VALIDATION.md, review cleanup; leaf.rs, Leaf; RT-04; ARENA-HOON-IR.md, lifetime and unwind safety.

The second place was memoization and here the tension was measurable. Every type-checker cache in honk is supposed to be a pure accelerator: a hit must be indistinguishable from a miss. Twice that rule was broken by omission. The first time, a memo that was sound for the isolated prelude compile was left on for kernel compiles, where the mutable state it reads drifts as the compile proceeds, and a memoized verdict flipped. The symptom was not a wrong artifact but a spurious redo-match failure on the Roswell kernel, and the fix was to scope persistence to the one compile where it is sound. The second time, an adversarial audit of every cache surface found seven, mint, mull, redo, rest, fish, nest, and crop with fuse, whose keys omitted the active %hold fan scope, so an entry computed under one recursion context could be reused under another. Two existing tests had encoded the bug by asserting exactly that cross-scope hit, and had to be flipped. Widening the keys was output-neutral on every kernel and cost real time: Roswell went from 53 seconds to 68 with the fan context in the key and to 75 with the arm-epoch context, over the 60-second gate I had set for myself. I shipped it over the gate. A correctness property you can name is worth more than a number you picked, and the arena work later recovered the time. The response to both bugs was not a resolution to be more careful but a written inventory of every cache in the engine with a verdict for each, delete, re-key, or preserve, and the semantic context each key must carry. Sources: OSS-NEXT-PLAN.md, roswell redo-match resolved; OSS-NEXT-PLAN.md, H2 cache-soundness audit; PHASE0-CACHE-MATRIX.md, executive summary.

The mirror image happened too. A first attempt at interning types after construction was byte-exact on all six kernels and made Roswell slower, 71 seconds to 84, because confirming a candidate match meant walking a core whose size grows with the subject, and kernel cores are mostly unique, so the cost was never repaid. It was reverted, and the version that eventually landed interns at construction on child identities, where confirmation is one shallow compare. Being right was necessary. It was not sufficient. Source: OSS-NEXT-PLAN.md, post-construction interning reverted.

There is one place where the accelerator rule is not yet fully honored: The native mint, mull, and core_mint caches identify the gene by a 64-bit structural signature and store only the result, so a hit is not confirmed against the gene the way the noun-keyed caches confirm theirs with an exact compare. The subject and goal in those keys are exact arena identities, so a collision needs two different genes with the same signature under the same subject, goal, and context. The birthday bound puts that around n squared over two to the sixty-fifth, and the mixer is not cryptographic. The fix is mechanical, it would be a bucketed entry confirmed by comparing the gene. Sources: intern.rs, native mint, mull, and core_mint caches; mint_cache_lookup.

The third of our places where tension arose was approximations that were correct only because of the environment they grew up in. NockVM's dor jet decided whether two heads were equal with a pointer comparison. On the interpreter stack that was right almost every time, because unifying equality had usually merged equal nouns into one pointer before dor ever looked at them. honk's nouns live in slabs that never unify, so the jet mis-ordered every time, and since dor breaks ties inside gor and mor, the shape of every map and set built through it diverged from the shape Hoon builds. The fix made the jet do what soft ++dor does, a mug pre-filter and then a structural walk, and it brought the jet into agreement with honk's own native comparator rather than the other way around. The same class of problem showed up in jet dispatch. %fast registration matches a core's battery against the recorded one, %spot hints bake source positions into batteries, and two compilers emitting semantically identical code at different coordinates produced batteries that never matched, which silently lost every jet beneath them. The matcher learned to ignore transparent hints while keeping axes and constants exact, and because that comparison is expensive it is a dispatch mode that honk opts into while the node and hoonc keep exact matching. The lesson I take from both: a fast path whose soundness depends on an invariant of its environment is a latent bug, and a new client of the runtime will find it. Sources: DOR-DEEP-EQUALITY.md; sort.rs, structural head comparison in dor; BATTERIES-MATCHES-STRUCTURAL-EQUALITY.md; cold.rs, nock_formula_eq_ignoring_transparent_hints; jets.rs, JetDispatchMode; honk selecting HintBlind.

So what did I give up? Purity at the implementation level, without apology. The arenas are mutation-heavy, the allocator is jemalloc, the hot paths are unsafe, and there is no ST monad standing between a handle and the arena it points into. What I did not give up is referential transparency where it can be observed. The same source produces the same bytes on every host, with the cache or without it, under PGO or not, and the build checks that on every run. Purity inside the compiler was a means. Determinism of the compiler is the end, and it is the only one of the two that anyone downstream can verify. Sources: build-honk-pgo.sh, byte-identical verification; ARENA-SEMINOUN-IR.md, correctness gates.

That is also why every design record in the repository ends the same way, with the SHA-256 of six kernels and a test count. I'll end this article in the same way as my spotlight, with a point about zero-knowledge proofs that I keep coming back to: don't tell me you performed the computation, give me a verifiable proof. Applied to engineering claims, it means a performance number without an exact-output hash beside it is an anecdote.