What I did with Monad the last 2 weeks: Oak, a web stack, and a path toward univalence

October 31, 2026

The last two weeks were the busiest stretch this repository has seen. Between October 16 and October 30 the tree took 370 commits — roughly
185,000 lines added and 53,000 removed — and it did not spread those
commits evenly: October 18 and 19 alone saw 96 of them. Still a lot of work remains.

The priority is to stabilize the language features and ensure they cover enough. Two threads dominated. The first is a small fleet of library motes that turned out to be the foundation of a web stack — a spec-complete Markdown parser, an Elm-shaped HTML layer Oak, a browser runtime, an HTTP server Moon, and a browser REPL assembled from the same parts. The second is the language itself: dependent-type machinery moving toward cubical primitives, values are now affine by default (use 0 or 1 time, like in Rust), and a toolchain with monadup for loading the latest release.

One experiment ran alongside both: weaver, a coding agent written in Monad — unfinished, buggy, and still the most demanding program the language has to run. Really pushing the limits of what the runtime can do today and providing a lot of valuable insights. It works, somewhat, but more work is needed.

Here is a summary of what has been done, created with the assistance of LLMs of course. I also notice a lot of the limits to what LLMs can do today and I think we easily fool ourselves into thinking their capabilities are greater than they are.

Also I worry about the energy consumption, environmental impact and lack of European alternatives. All of which is something I am working towards, but AI can be incredibly useful for some tasks. And for this project it has been essential to move so fast and with quality.

Markdown

The motes/markdown mote — added October 28 — is a CommonMark 0.31.2 + GFM parser that passes all 652 spec examples byte-for-byte, plus GFM tables, task lists, strikethrough and autolinks. It is total: any byte sequence parses to a Document, with no error branch and no Result. Pathological nesting degrades to literal text at a configurable depth rather than failing.

It is also renderer-neutral and composes with the rest of the stack, since to_html produces the same xml_html nodes that oak and the site generators use. The entity and Unicode tables are generated by Monad programs built on a new gen mote and lang::construct (the compiler's own term builders and surface printer), and --check on either tool verifies the committed tables are current.

The web stack: oak, moon and the wasm runtime

The ongoing full stack web framework experiment got a lot of progress. Oak and moon came together into something recognizably a framework, and its two ends — the view and the wire — each get a closer look below. Still a lot of work remains to stabilize it and smooth the rough edges.

Oak: event sourced web apps

Oak is type-safe HTML with an Elm-inspired surface. The builders are ordinary functions returning Oak.Node Msg — Html.div [attrs] [children], Html.text — over a curated attribute set, with Html.attr/Html.bool_attr for the long tail:

def card {Msg : Type} (title : String) : Oak.Node Msg :=
    Html.div [Html.class_ ["card"]]
        [ Html.h1 List.empty [Html.text title],
          Html.p List.empty [Html.text "from Oak"] ]

(Attribute names that collide with Monad keywords take a trailing underscore — class_, type_, for_ — and the emitted attribute never does.)

The interesting type is Oak.Node Msg: a thin wrapper over the shared xml_html markup ADT, parameterized by the message type. An attribute is either a real Html.Attr or an event binding, and an event binding is just a pure function WebEvent -> HandlerResult Msg. There is no decoder to write and no numeric handler id anywhere in the surface:

Html.button [Html.on_click Msg.increment] [Html.text "add"]
Html.input [Html.on_input (fn (s : String) => Msg.set_text s)]
Html.div [Html.on_dragover Msg.over, Html.drop_effect "copy",
          Html.on_drop (fn (e : WebEvent) => Msg.dropped e.data)]

The same view serves the server and the browser because lowering is the boundary. Oak.lower writes each binding as a data-oak-on-<event>="<id>:<flags>" attribute and returns the id → handler table; Oak.to_html, the SSR path, simply drops the onattributes. The ids are FNV-1a hashes of the node's patch path plus the
event name, so they are stable across renders and already correct when the patcher mounts a lowered subtree at an arbitrary path.

Around the views sits the rest of the Oak architecture, and it is host-agnostic by construction. Program S Msg E is pure data — an init model, an update : S -> Msg -> Pair S (Command E Msg), a view : S -> Oak.Node Msg, a subscription list — and Command has exactly four constructors: none, quit, dispatch, perform. The counter is the whole shape:

type Msg {
    increment,
    reset,
}

def update (model : I64) (msg : Msg) : Pair I64 (Command Unit Msg) :=
    match msg {
        Msg.increment => Pair.pair (model + 1i64) Command.none,
        Msg.reset => Pair.pair 0i64 Command.none,
    }

def view (model : I64) : Oak.Node Msg :=
    Html.div [Html.class_ ["counter"]]
        [ Html.button [Html.on_click Msg.increment] [Html.text "add"],
          Html.button [Html.on_click Msg.reset] [Html.text "reset"],
          Html.span [Html.id_ "count"] [Html.text (I64.to_string model)] ]

def app : Program I64 Msg Unit := Program.app 0 update view

A host — the wasm loop in oak_wasm, a test monad, a server — supplies a Host N E Msg that interprets effects, and Program.run_batch folds a batch to quiescence under any Monad. The batch semantics were ported from the TUI's event loop rather than reinvented: dispatch queues a message for the next batch, perform runs its effect immediately and folds the resulting message into the current one, and quit stops the fold. Subscriptions are the fourth leg, declarative in the same way handlers are:

def subs (_m : Model) : List (Subscription Msg) :=
    [ Subscription.window_msg "resize" Msg.resized,
      Subscription.document_msg "visibilitychange" Msg.hidden,
      Subscription.animation_frame_msg Msg.frame ]

For whole documents there is HtmlT, an index-tracking page-assembly transformer (Render M -> Page -> M (Pair Page A)) whose phantom lifecycle types — Open → Sealed → Emitted — turn "I wrote to the headafter sealing" into a type error. Its production stack is PageM, a ResultT String IO newtype that ends in Ssr.render_io : HtmlT PageM Open Emitted Unit -> IO (Result String Response): a whole page assembler lands as an http.Response. The dependency direction is deliberate — the adapter lives in oak, so a JSON-API server depending on moon never pulls the markup parser into its closure, and moondoes not depend on oak at all.

Two footnotes in the project's usual register of honesty. Page assembly is handler-free by design: a browser view that needs handlers is an Oak.Node Msg assembled by the client runtime, not a Page.

oak_wasm — the browser runtime: a pure diff over Html.Node, a DOM applier, and the mount/dispatch/tick loop an app exposes through three #[export "c"] thunks. It gained SSR hydration (the client adopts the server-rendered tree), a keyed list diff so reordering preserves DOM nodes (a child stamped with oak's Html.key is reconciled by key, not position), and a working single-page app.

Moon: the HTTP server

moon is the wire side of the stack, and its shape is the opposite of Oak's: where Oak wraps one markup ADT in a typed view, Moon keeps everything a plain function. The router is pure data in, response out — a List Route with :param captures:

use http::types {Request, Response}
use moon::router {Route, Router.get, Router.param, Router.route}

def show_user (req : Request) : IO Response :=
    match Router.param "id" req {
        Option.some id => IO.pure (Response.ok_text (String.concat "user " id)),
        Option.none => IO.pure (Response.ok_text "no such user"),
    }

def routes : List Route :=
    [ Router.get "/health" (fn (req : Request) => IO.pure (Response.ok_text "ok")),
      Router.get "/users/:id" show_user
    ]

Method dispatch is handled the way it should be: the first matching route wins, HEAD falls back to a GET route (the server suppresses the body), a path that exists under other methods answers 405 with an Allow header, and OPTIONS on a known path answers 204 with Allow.

The canonical handler type is Request -> IO (Result String Response) — a failure is a value, not an exception, so Handler.recover is a real adapter — and middleware is literally function composition:

use moon::handler {Handler.of_response}
use moon::middleware {Middleware.cors, Middleware.logging}
use moon::server {Server.serve_result}

def app : Request -> IO (Result String Response) :=
    Middleware.logging (Middleware.cors (Handler.of_response (Router.route routes)))

def main : IO Unit :=
    Server.serve_result app 8080u16

(logging, cors, content_type, recover, auth_basic and auth_bearer ship in the mote; Server.serve takes a total Request -> IO Response handler instead.)

Two servers run the same handler. Server.serve accepts connections one at a time and keeps each alive — a pipelined request is served out of the bytes the previous read left behind. Server.serve_concurrentruns a fiber per request with a bound: it accepts up to max_in_flightconnections, forks a handler fiber for each, then drains the batch before accepting more — and forkIO is not lazy, so handlers really do run concurrently with the next accept.

On top of that: byte-exact static assets (a traversal guard, MIME types, ETag and range requests), cookie-backed sessions — an in-memory table whose ids are a SHA-256 of nanoseconds, process id and a counter, documented in the module itself as not a CSPRNG, with rotate to defeat fixation — and CSRF tokens derived from the session id and compared in constant time. There is even a development loop: Live.watchpolls a file's SHA-256 every 500 ms on a fiber, and Live.reload is an SSE endpoint that emits a reload event per change. Polling, not inotify — there is no file-watcher native, and 500 ms is enough for a development loop.

The known gap is documented in server.mo's own header: a peer that opens a connection and then says nothing holds it until it closes. max_keep_alive_requests (100) bounds a talking client, not a silent one; a real fix needs a socket read deadline the IO layer does not expose yet.

Under all three sit shared pieces (all new or heavily reworked this window): xml_html (shared HTML/XML nodes and a linear serializer), jsgen (a controlled JavaScript emitter), web_wasm (the wasm-only browser boundary) and web_event (typed DOM events, drag-and-drop, clipboard and subscriptions).

Language and type theory

Cubical type theory provides a practical route to Univalence support. The benefit of this is the ability to transport and use the equivalence of proofs and types. The self-hosted compiler kept moving on the things that make Monad Monad:

Cubical primitives. hcomp, the is_one witness, path combinators (refl, sym, ap, apd), and finally Glue — the former, the introduction and the elimination — landed, each pinned by a proof in the proofs mote. Path, isContr, fiber, isEquiv and Equiv are in place: the road to univalence now has every stone down, even though there is a long way to walk.
Elimination with a real motive. if/match now elaborate into an Elim node with an explicit motive, and whnf gained iota reduction for it — including a non-constant motive derived from a bound-variable scrutinee.
Affine by default is enforced. An unannotated binder is ≤1 unless Copy A resolves, on every check and compile path; Shared replaces the old Borrow, and views, Clone and function moves came with it. Motes mid-migration carry a per-mote [affine] mode = "warn" escape hatch.
Type classes get stricter. A def's declared class constraints are now enforced at the call site — a missing instance is reported at a bare constrained reference and at a class-method call, instead of silently type-checking and failing at run time.
The checker enforces its own rules. Visibility is enforced at every reference, use-completeness is enforced, and each checked file gets its own module scope with cached, reused checks across the corpus.

Runtime and concurrency

A quiet but important thread: the runtime got race-condition discipline. Over a handful of days it pushed nullary-constructor caching atomic, locked the child-process registry and the per-descriptor read-ahead table, made every pipe and socket close-on-exec, and added a thread-safety stress gate. On top of that, fibers now cancel cooperatively at the next IO bind, abandoned fibers free their stacks, and std/concurrent gained MVarchannels, select, race (returning the first to finish) and timeout.

Toolchain: it ships itself now

October 19 was a toolchain day. monadup — the Monad-written version manager — got its bootstrap stub and nightly assets: curl … | bashinstalls it, and it then manages nightlies under ~/.monad for x86_64-linux, aarch64-darwin, cross-built aarch64-linux and an experimental riscv64-linux, with static Linux binaries and a macOS build linking only libSystem. monadup doctor checks the LLVM/GC build prerequisites for you.

Around it: a wasm target (wasi and web proofs, a loader, and a CI leg), and a monad repl command over the shared evaluator. Weaver's CLI moved to clap's derive, and the Rust host workspace moved under rust/ with shared workspace dependency inheritance. The shared evaluator's most public front — the browser REPL — is worth its own section.

The browser REPL: the compiler in a Web Worker

Try it here now.

monad-lang.org/try looks like a scratchpad; the machinery under it
is the actual checker and evaluator. The whole pipeline — the self-hosted parser, scope
builder, typechecker, lowerer and CoreIr interpreter — is compiled to
wasm32-unknown-unknown and runs in a Web Worker, so a visitor's program is checked and evaluated on their machine, with no server round trip.

It is split into two motes with a hard boundary. try_engine is the evaluator and is deliberately DOM-free — the Oak UI is a separate mote, so the engine never links browser code. try_ui is the page itself, and the page is an Oak program: the same Program/update/viewlayer the web stack section describes, running one hand-written host.

The design decision worth stealing: the prelude is not compiled in. The page fetches the real init/src/*.mo files served beside the wasm and hands their text to the engine as a length-prefixed payload, which the engine parses back into module identities. A /try program is checked against exactly the sources the site ships, and a module added to init/src becomes usable in the browser without touching the engine.

What you type follows one convention, mirroring monad eval: the program must define a main, and main's value is the result. One of the shipped examples:

def describe (o : Option I64) : String :=
    match o {
        some x => String.concat "got " (I64.to_string x),
        none => "nothing",
    }

def main : String := describe (Option.some 42)

The engine is the shared evaluator's third front: monad eval, monad repl and /try all run the same recipe — the standard source-list loader and the one typecheck/elaborate/lower/evaluate pipeline — so the browser is not a toy dialect but the same checker over the same prelude. What stays in try_engine is /try's own policy: a 256 KiB source gate ("/try is a scratchpad, not a build service"), two million steps of fuel, a 200-call depth cap tuned to the web profile's stack (a clean "the program recursed more than 200 calls deep" beats a wasm trap), results clipped at 8 KiB — on a UTF-8 boundary, so a truncated value never ends in U+FFFD — and rejections with manners: std and IO are refused with "not available in the browser REPL (the ambient prelude only)", and use lib:: is told to name a module explicitly.

The UI has two details worth copying. The editor is uncontrolled: typing updates the model but not the rendered text, so the caret and the undo stack survive re-renders. Loading an example bumps a monotonic key that remounts the textarea — the keyed diff from oak_wasm doing real work, not a demo trick. Run starts the worker, an animation-frame subscription polls it until the result arrives, and Cancel terminates the worker — which is also how a runaway loop is cancelled.

The ecosystem motes

The window added or matured a long list of libraries: crypto (RS256, ES256 and EdDSA verification through OpenSSL EVP, plus a RAND_bytesCSPRNG), jsonwebtoken (JWT/JWKS/claims), oauth, streaming HTTP with SSE and chunked bodies, yaml with a serde backend, time with ISO-8601, sql and sqlite, and log (a LogT transformer with JSON-lines output). A new clap mote, an xml_html core, and the gen/constructcode-generation pair round it out.

Weaver: the experiment

And now the experiment. motes/weaver is a coding agent written in Monad, built on motes/shuttle — the typed tool-use harness — and it
went from a line-based approval loop to a streaming,
session-persisting, MCP-mounting terminal application in fourteen
days. It is also still an experiment with many bugs. What it is:

A policy engine and mode state machine. manual → plan → allow_edit → auto, with the whole safety story in one pure capability × mode → decision table.
A TUI. On October 17 it moved onto motes/tui's generalized run_app; since then it has gained a streaming turn display, mouse wheel scroll, drag-to-select with OSC 52 clipboard, multiline input with prompt history, a model picker, and approval dialogs that render the diff for a proposed write or edit.
Sessions on disk. ~/.weaver/sessions/<id>/ stores the transcript, per-turn model history and metadata; the TUI keeps only a 512-line window and pages older blocks back from disk, so memory stays bounded while the full scrollback is reachable. --resume and --continuepick sessions back up across restarts.
Streaming, retries and compaction. Turns run on a fiber while the UI keeps folding keys; failed provider calls retry with backoff (but not on a 4xx); /compact summarizes context through the same model, and autocompact fires automatically before a turn when the estimate crosses a threshold.
Monad-aware tools. monad_check runs the compiler's own checker on a file or an in-memory buffer, and monad_eval runs a REPL-style scratch module on the self-hosted interpreter — with a step budget and nesting cap so a runaway snippet returns a tool error instead of pinning the turn.
Subagents and MCP. A read-only task subagent runs one bounded child loop, and external MCP servers mount with --mcp <executable>, their proxy tools defaulting to exec capability.

For all its bugs, weaver is the most demanding test the language has: the whole loop is driven offline against a scripted mock wire, 11 scenarios over a synthetic slow provider, gated in CI — and the README documents what weaver does not do (no fsync, no sandbox, auto mode is a trust setting rather than a jail) as carefully as what it does. That honesty is the experiment earning its keep.

The shape of the fortnight

Pull back and the story is coherent. A big chunk of the work was infrastructure that had been sketched and is now real: a web stack, a toolchain, and a parser that passes a spec. The most interesting output is the pair at the ends of the spectrum — the browser REPL, which puts the whole compiler in a tab and checks a visitor's program against the very sources the site ships, and the cubical primitives, which push the type theory toward its most ambitious goal. Weaver, the experiment, sits somewhere between: too rough to headline, too demanding to ignore — nothing else in the tree exercises the language under real concurrency, real IO and real streaming the way it does.

If you want to try any of it, monadup default && monadup doctor gets you a nightly, and monadup new hello scaffolds a project. The full
area-by-area state of things lives in the Maturity Matrix — measured against the
compiler's own source and tests at this commit, not inferred from intent.

370 commits, one author, fourteen days. The tree is still alpha, and the README still says so; but it is steadier every week.