~sarlev: What first drew you into the idea that we needed to throw away and rewrite the entire networked computing stack? Or is that not quite how you came to this work?

~navsul-pagrec: It is not really an Urbit conversion story for me. I bought an Urbit star when they were selling them for $512 during the fundraising round, but I think I booted something once and that was roughly the extent of my direct engagement. Urbit and Bitcoin inhabited the same category in my head: they were aligned with problems I cared about and I hoped they succeeded, but I was not sold on the particulars of either approach. They were interesting things other people were working on, but not a specific platform I was going to invest time into.

What kept my attention was the underlying domain problem. I want people to own their own compute/data and be able to coordinate without handing everything over to an advertising organization. That's compelling to me. I did not need to accept every detail of the Urbit's thesis to see that.

Nockchain made part of that problem space high-leverage and tractable for me. I also knew and trusted some of the people involved. When I spoke with Zorp I found the case for utility was compelling. Nockchain's approach to permissionless, distributed/p2p, general-purpose compute made intuitive sense to me even though I wasn't a "crypto native." I work on a small deterministic machine, Nock, and my work pursues a very practical question: how do we make this useful and reduce the friction for new developers and users? The principal philosophical differences I think lie in Nockchain being simultaneously an L1 blockchain, a cryptographic currency, and an application platform all at once. The full-ZKVM ships by EOY, but the current instantiation of Nockchain has relied on NockApps to leverage the ZKVM and blockchain state since before the chain launched.

~sarlev: What did you initially do at Zorp and how did developer experience become the immediate problem instead?

~navsul-pagrec: I was originally hired to work on an optimized GPU prover for the ZKVM. Nockchain had a fair launch and we needed a competitive miner to fund platform development. We weren't granting ourselves Nock issuance by fiat. There were enough developer-experience blockers early on that it was difficult to begin seriously pursuing that work.

When I started running or testing Hoon code meant manually firing up an Urbit Dojo and loading things. I did not have a good way to run batch CI jobs or kick off an evaluation from a normal POSIX terminal and inspect the result. I was not going to tolerate that. Not just because it was uncomfortable for me, but because we could not build a productive engineering process around it. It was required for soundness and verification as well: I needed static, cacheable, inspectable compilation artifacts that existed independently of the rest of the application state. I'm familiar with similar patterns such as Lisps like sbcl having core files (runtime memory snapshots), but it adds too much friction to separately verify the integrity of codegen and application data. Application data in our case is blockchain state and that requires a lot of care.

My colleagues took mercy on me and we started building bridges. One was originally called choo, which eventually became hoonc: a NockApp around the bootstrapped Hoon compiler in Nockchain's pinned Hoon prelude, %138, that could produce reusable build artifacts. We also made utilities--kicker, later named hoon--for compiling and running traps from the command line. The Nock runtime that runs everything is ~ritpub-sipsyl's NockVM, neé Sword, neé Ares. I worked on build times, caching, and an aggressively tuned Bazel build for Zorp's internal monorepo. On the happy path, warm cache and relatively low churn, we got builds down from an hour and a half to three and a half minutes. Much of which was running an unconditional benchmark, not the build itself.

That is the recurring theme in most of my Nockchain work: getting the flywheels spinning faster. Shorter developer iterations. Faster CI. Better observability. Faster provers. If the feedback loop is slow, every other problem becomes harder. I've also worked on and optimized NockVM itself. My most prominent NockVM effort was the persistent memory arena which made it possible to have a peak RSS of ~1.5 GiB for a NockApp with an Arvo--subject--exceeding 16 GiB.

~sarlev: Who pays the price when that feedback loop is slow?

~navsul-pagrec: For most of Nockchain's life, the main users were core developers, mostly Zorp people at first and now an alumni network plus other developers building on top of the platform. The most common user persona impacted by build times was someone firing up a node for the first time or updating one. We haven't historically distributed binary releases for security & transparency so every new user has to build the NockApps kernels, the Nock generated from Hoon, and the Rust framework wrapped around them.

Developer experience affected how quickly we could test consensus changes, how confidently we could update the chain, and how efficiently people could work on NockApps. The Nockchain wallet, a NockApp named nockchain-wallet and exposed via a CLI interface, is a good example. It touches a large portion of the system and quite reasonably had a lot of Hoon unit tests. Slow compilation became a significant drag coefficient on changing or extending the wallet NockApp.

That problem becomes more important as the audience grows beyond core developers. A person cloning Nockchain and setting up a NockApp--which instantiates its own data-dir, equivalent to an Urbit pier--for the first time encounters the cold build time and not the carefully warmed environment of somebody who has worked in the repository some time. If that first build is brutal, you lose people before they can do anything interesting. Let alone a developer iterating on a NockApp/ZK app built on the platform.

~sarlev: You said the case for Nockchain utility is what kept you involved. What is the human-scale version of that case?

~navsul-pagrec: Compute markets are where I have the strongest convictions but it generalizes beyond that too. Imagine a bright high-school student who wants to run a machine-learning experiment but cannot afford a quarter-million dollars of hardware in a shed. I grew up poor. If I wanted money for something, I had to skip lunch and save the lunch money. That is the kind of economic constraints I have in mind.

The ideal is that you do not even have to pay for a machine by the hour. You pay for the workload. You submit a training batch or another computation, the market distributes it, and the result comes back. A little like AWS Lambda, except not insanely expensive and dumb. In this hypothetical you could do the initial R&D on a local GPU in a gaming rig before iterating on larger training batches.

Doing that in a distributed environment raises two different problems. The first is faithful execution: did a provider actually perform the computation it claims to have performed? That is broadly the problem ZK proofs address. The second is privacy: can the provider perform the work without recovering the private inputs or traces? That is much harder, especially for inference. I do not want to conflate these problems. Solving faithful execution does not give you private inference and privacy schemes for inference don't usually provide a faithful execution guarantee by themselves either. These guarantees are critically necessary for the economic viability of any trustless compute market. Without one or both of these guarantees there is no reason for an inference/ML training consumer to pay even a marginal token premium for the extra compute required to bundle a ZK proof with the workload. There's a lot to be gained from the compute capacity and transactional frictionlessness such a system would unlock, which is why we're working so hard toward it.

~sarlev: Why not just use something like an OpenRouter endpoint that runs in a TEE? Or even just that routes to the cheapest provider?

~navsul-pagrec: OpenRouter is clearly aware of the faithless inference problem and it's been researched and published about elsewhere too. Inference customers should ask themselves how inference on platforms like OpenRouter can be so cheap. My understanding is that some Chinese inference providers subsidize their low prices by retaining inference traces and selling them to Chinese AI labs. OpenRouter has regional and privacy/zero-data-retention filters for inference customers, but I don't know how they could possibly enforce that. A dropdown option or modest privacy premium is not proof that a sufficiently motivated provider cannot recover your workload, even with hardware trusted execution environments.

There have been many proposed systems for private inference that were defeated soon afterward with effectively complete trace recovery. Weight activations leak an enormous amount of information. Batching can make a workload noisier, but it doesn't do anything for privacy and often makes inference non-deterministic. Non-determinism in batched inference pipelines is one of the principal problems you have to solve for verifiable inference. Without batching inference isn't economically viable for the long-haul. An interested reader could look at the time between when a proposed inference privacy solution is published and how long thereafter a PoC extracting the trace is published. It's a brutal problem space.

Verifiability and privacy both matter, but you need verifiability first. A useful compute market needs offline-verifiable proofs that the provider faithfully performed the work that the customer paid for. Ideally while revealing as little as possible about the work itself as well, but that is more difficult and will be a follow-up milestone to verifiable compute. ZK gives us a lot of options for addressing faithful execution even with computationally expensive workloads like inference. Privacy still has real research questions and ZK gives us a powerful toolkit for pursuing that too.

~sarlev: Where does Nock fit into making that verifiable-compute layer practical?

~navsul-pagrec: Nock turns out to be a very good foundation for a ZKVM. I tried to find a better alternative for some time. One alternative I considered was the 6502 because it is relatively simple and already has many high-performance emulators. Even something at that level of complexity exponentially increases burden on making the ZKVM scheme sound and on efficiently producing and verifying the ZK proofs.

Nock is a tiny instruction set operating over nouns. The relationship from Hoon to Nock is comparatively direct, which is useful when the output will execute in a security-sensitive context. You still have to build arithmetic circuits for approved ZKVM operations or "jutes." Jutes are jets permitted for use in the ZKVM which is embedded in the ordinary Nock execution environment. Careful tradeoffs between security, prover efficiency, verifier efficiency, and programmer ergonomics are required. Nock as a ZKVM substrate does not require modeling a modern CPU which is far too complex for this domain.

The larger utility story is that, once the right building blocks exist, developers should be able to recombine them into NockApps without requiring a new consensus upgrade for every application. A privacy pool, an off-chain storage service, or some other verified workload becomes a program assembled from available primitives rather than a new single-purpose chain. Developer experience lowers the friction at the beginning of that maze; useful ZK applications put stinkier cheese at the end.

~sarlev: You have a reputation for using LLMs very heavily. How did that become part of your engineering process?

~navsul-pagrec: I started relatively early with coding models, back when the main interface was intelligent autocomplete. One thing I noticed while writing Rust was that if I began Haskell-style with the types--write the function signature and give it a name that clearly expressed my intent--the model could often get me eighty or ninety percent of the way there. Sometimes it got all the way there, although the models took more shortcuts then.

My adoption has been aggressive in volume but conservative in method. I make modest changes to the workflow, see if they hold up, and then keep moving. I went from autocomplete, to an agent window in the editor, to command-line agents, and now I mostly use desktop GUI applications for my inference harness. I do not build an ornate orchestration harness unless I have a specific and limited-scope reason for doing so. Part of that is taking the bitter lesson seriously: the models improve quickly enough that elaborate scaffolding can become obsolete in months, not years. When I'm not using one of the desktop GUIs, I'm usually using omp or looking something up in the interface. I don't remember the last time I googled something work-related.

Another reason is that I want an untainted sense of a model's strengths, weaknesses, and personality. I move between two or three models depending on the task. When I am on shakier ground I will have a fresh session or a different model red-team the work. I know this isn't novel or unique, but I have run councils where several models debate a decision, although that is less necessary now than it used to be. Manually refereeing a two-sided debate is often sufficient for prosecuting even some of the more difficult and complicated work I do.

I also use them to learn, not just to get work done. This is under-discussed. I can ask the model questions. I can ask the model which questions I should be asking. I can give it context on my background and I'm already familiar with. It's an infinite-patience tutor and it can lead you to the most relevant parts of the original sources. I can fan out performance experiments, study which ideas fail, and ask the models to explain what happened. NVIDIA's documentation will tell you that every CUDA feature is useful. Running out two hundred branch-experiments tells you which features are actually useful for the workload you're optimizing.

~sarlev: What makes that process trustworthy enough for work on compilers and ZK provers?

~navsul-pagrec: The project has to give you enough assurance that you can safely delegate a bounded task. I have types, tests, production monitoring, and a way to roll back. If you cannot imagine giving an appropriately scoped ticket to a junior engineer and merging it when the checks are green, that may indicate that you need better tests or observability regardless of whether you use an LLM. Some work is always going to require single or multi-human review, especially security-sensitive work, but you should be working to improve the leverage ratio between what AI can accomplish autonomously vs. what requires a human in the loop. AI didn't fundamentally change this. Push-on-green CI/CD pipelines have been the gold standard in the software industry since well before transformers were invented. I have used languages like Rust and Haskell which are known for their strong, expressive type system for over half of my career. I even wrote a Haskell book to ameliorate the friction and unfamiliarity of Haskell for developers and new programmers. I care about types not just because I want a correct program but also because machine-verifiability enables you to go faster and take down bigger game.

An important conceptual tool I use for working with LLMs is "show your work." It is one thing to tell a model to do something. It is another to anchor it on the evidence and data it gathered while doing the work. Asking for evidence makes it less likely to take shortcuts. If I am worried, I ask another model to challenge the result. The models can bicker with one another while the artifacts, tests, and measurements settle the argument.

This principle is not so different from zero-knowledge cryptography. Do not merely tell me that you performed the computation. Give me an efficiently offline-verifiable proof that you did it faithfully.

~sarlev: How did this all lead to building "honk"?

~navsul-pagrec: We needed a much faster Hoon compiler. It was not optional if we wanted the Nockchain utility flywheel to get moving. There are a lot of dead bodies in the ditch labeled “tried to make a new Hoon compiler,” so skepticism was reasonable. I pushed NockVM's efficiency within the constraints of the current architecture as far as I could. This effort made both hoonc and NockApps, including the blockchain peers, faster. But I hit a limit eventually and the next step on NockVM efficiency is likely designing a bytecode VM for it. The bytecode VM will likely have implications for ZKVM soundness and verifiability so I'm planning to pursue that after the full ZKVM has a stable release. I knew that if I wanted a faster compiler I had to write a native Hoon compiler. Native meaning most of the runtime is statically compiled & optimized Rust.

A new compiler that already has a spec implementation is an advantageous starting point for an LLM-assisted process because I had two strong truth anchors. First, I had Nockchain's pinned Hoon-138 compiler running through hoonc. We were writing Rust, but we could follow that implementation closely instead of re-inventing semantics and logic. Second, I had the artifacts persisted to the native filesystem that I could compare. If the jam did not match, there was a problem. This description glides over the frictions somewhat. I had to iterate on a CLI tool for detecting and backtracing differences in jammed Nock nouns several times over the course of working on honk before I had something that was reliably useful to both myself and the AI agent. The final result of that was the jam-diff utility. There's some tension between what's most economical for an AI agent and what's most legible to a human in a debugging utility like jam-diff. When there was a trade-off to be made I chose mechanical sympathy almost every single time. I wedged human legibility into the gaps of that edifice.

hatch is the native parser and honk is the native Hoon-to-Nock compiler and build driver. The parser was one of the hardest parts because Hoon's grammar is more performance art than engineering. Parser decisions affect source locations and debug hints even when the resulting Nock formula is otherwise correct. Most of hatch (the parser) came from a contributor who created an excellent foundation that I was able to build on. My work on hatch mostly involved implementing missing syntax--markdown, %sail syntax, and doccords--and a long tail of parity fixes. Once I had native ASTs in Rust from hatch I was able to get traction on the compiler itself.

The LLMs supplied a great deal of mechanical leverage: code archaeology, ports, experiments, and tests. The human work was choosing invariants, deciding what evidence counted, interpreting failures, and discarding changes that did not survive measurement. A great deal of human taste was required as well. Taste affects how you approach debugging, efficiency, architecture, all of it. A model can turn the crank very quickly, but you won't get a result you're happy with maintaining in a reasonable amount of time without human judgment guiding the process. It's more akin to a software factory than a fully autonomous artificial general intelligence at this stage. Programmer-as-millwright.

~sarlev: What is actually different about Honk, and what did that change in practice?

~navsul-pagrec: hoonc isn't deliberately slow by any means. hoonc is a relatively minimal NockApp built on Nockchain's canonical Hoon-138 compiler. It ships with a prewarmed state, uses jets, and has parse and build caches. hoonc uses the same six memoization jets as Urbit does for its compiler. But the compiler and build system still executes as Nock--compiled from the Hoon prelude--through NockVM with compiler structures represented as nouns that have to be allocated, traversed, and compared. There are fundamental limitations to what optimizations you can perform when you're working with an abstraction as a general-purpose as a Nock runtime. Taking ownership of the entire build pipeline--parsing, compiling, emitting Nock--unlocked significant scope for optimizing the application.

honk parses source and resolves imports in Rust and has direct implementations of the typechecking and minting operations against a native intermediate representation. It is not totally free Noun data or Nock execution as of yet: it still invokes NockVM where compile-time evaluation is required. However, in my latest honk milestone, which is 20x faster than hoonc, there are actually two Nock interpreters. One is a much lighter weight and faster harness for minimal const eval cases that don't call out to any Nock arms. In cases where you hit a Nock 9, it falls back to evaluating in NockVM. The compiled Nock of the Hoon prelude is embedded in the compiler so that you don't have to bootstrap the prelude on cold builds. The first native version was about four times faster on the relevant cold builds, but it still reproduced too many of the old structural costs. The large gains came from representing Hoon syntax trees, types, formulas, known values, and partially known values as compact canonical DAGs with efficiently comparable identities. There are specialized equality routines in honk for both Nouns in general and for the native intermediate representations. Instead of repeatedly reconstructing a tree and asking whether two enormous nouns are equal, many operations can compare scalar or tupled identities and safely reuse prior work.

Nockasm, from ~lagrev-nocfep, then gave honk a useful representation for inspecting differences and persisting shared build products. With Nockasm integrated, Honk now supports content-addressed incremental compilation without replacing jam as the canonical final artifact. Serializing the IR to Nockasm was almost 2x faster than jamming Nouns. Nockasm also makes analyzing parity differences between the compilers significantly more human-and-machine friendly.

In medians of three isolated M5 Max runs reported in Nockchain PR #153, a cold Dumbnet build took 400.8 seconds in hoonc and 19.5 seconds in Honk, a 20.6× improvement. A comment-only root-churn incremental compilation benchmark went from 7.0 seconds to 2.2 seconds or 3.1×. The cold-build tradeoff is memory: about 1.2 GiB for hoonc against 4.1 GiB for Honk in that benchmark. honk's first release milestone where it was 4× faster had an RSS peak closer to 11 GiB so I've been able to make significant progress on the memory efficiency too.

Those are workload-specific numbers, but the only exception to the "20× or faster" build-time improvement thus far has been the Hoon prelude itself. The Hoon prelude is tremendously annoying to compile efficiently. "Cold" also means the compiler is building the artifact from scratch; both compilers used their shipped prelude bootstrap. The controlled Nockchain parity suite demands byte-for-byte jam equality, but that gives us strong evidence over the corpus, not a proof covering all possible Hoon. Test builds of sobchek's vesl project have exposed non-semantic %spot metadata differences--row and column numbers, sobchek has unusual import syntax--and a modified softed-constraints.hoon deliberately delegates its build to hoonc.

~sarlev: Does that mean Honk can replace the compiler used by Urbit developers today?

~navsul-pagrec: Not as a drop-in today. Honk is currently focused on Nockchain's pinned Hoon-138 environment. The native compiler core is the reusable part, but Urbit also has %ford, %clay, desks, marks, the current kelvins, runtime integration, and source-metadata expectations. Those are separate layers that would have to be modeled and differentially tested against Vere.

It also does not make an already compiled ship faster. Honk is a compiler. It can shorten build and edit loops in the environment it supports; it does not accelerate Ames or Gall event processing by itself. You could try to use honk's const-eval harness for limited runtime execution but I don't think it'd be profitable when Vere has a bytecode VM already.

The next things I want to ship around Honk are the language-server work and VS Code plugin and a more reusable compiler toolchain targeting Nock. The language server and VS Code plugin are already quite usable and fast but I need to rebase the branch onto Honk's frontier branch. The LSP already has parsing, typechecking, targeted diagnostics, go-to-definition for several kinds of entities, and types/context on hover. I would like to add CodeLens support and then support more editors, such as Zed. Nockasm functions as a linker-like format for compiled batteries, but longer-term I'd like to factor out a separate linker utility for Nock. I'm working toward making honk a Hoon frontend to a more general Nock compiler framework or backend.

An Urbit compatibility mode is something I would like to see, because it would be good to return value upstream to the ecosystem that produced Hoon and Nock. I can't be responsible for maintaining the Urbit particulars but I'd like the Urbit compatibility to live in-tree with honk and to collaborate on an ongoing basis with an Urbit counterpart. If someone is interested they should reach out and I'm happy to help them get started.

~sarlev: If you had not found Nockchain and this broader Nock-shaped corner of computing, what would you be doing instead?

~navsul-pagrec: I would probably be a kernel engineer at NVIDIA working on inference optimization. I am a generalist, but I really like performance work. When I worked on ordinary business software, data-at-scale is one of the few domains where you occasionally get let off the leash to do something interesting because the operational costs were large enough to justify it.

I believe this is a higher-leverage use of my attention at the moment. There are already many smart people working on inference kernels. I care about open models keeping the frontier labs honest, but the alternative ecosystem has to be technically credible and economically honest. Making compute markets cheaper, verifiable, and eventually more private seems like a place where my work can become significant.