#Building an application

A click can flash a ring and a tween can slide the chart, but neither can remember. The moment you need something that survives the click and decides what is shown next — a score that climbs, a document you can undo, a blotter of open positions — you have run out of canvas. That persistent, display-deciding state is the one primitive the first three planes deliberately withhold, and supplying it is the whole of the APP plane.

An application is four small things: a model, a pure update, a pure view, and a set of declarative subscriptions — the shape the functional-UI world calls The Elm Architecture (TEA). Effects are inert data the host executes; capabilities are default-deny; and one message journal is the single source of truth. That last fact is why so much falls out for free: an application built this way can be replayed message by message, tested without a single mock, and re-executed on a server bit-for-bit. This chapter builds a small application and follows each of those guarantees out of the one shape. The APP plane is strictly additive to the frozen core, and its rollout follows the v1 language.

Figure — everything ambient enters through the front door as a message; everything outgoing leaves as inert data the host interprets under a capability.

A note on the samples. A few samples below carry a member of an app block — an update, a view, a subs — outside its block. A member is only legal inside one, so read those as if the member sat within app name { … }; the type and def declarations beside it are ordinary top-level statements. Every unmarked sample is a complete program.

#The shape of an application

Here is a whole application. It counts up once a second and plays a sound when you reset it:

app counter {
  capabilities: [ clock, sfx ]        // `clock` backs OnTick; `sfx` backs PlaySfx — both are needed

  init(p)        = { n: 0 }
  update(m, msg) = match msg {
                     Tick  -> { model: m with { n: m.n + 1 }, cmds: [] }
                     Reset -> { model: m with { n: 0 },       cmds: [ PlaySfx("reset") ] }
                   }
  view(m)        = row {
                     text("count: {m.n}")
                     button("reset", Reset)
                   }
  subs(m)        = [ OnTick(1000, Tick) ]
}

Read it top to bottom and the loop reveals itself. subs declares that a tick should arrive every second, wrapped as a Tick message; update folds that message into a new model; view renders the model; the Reset button emits a Reset message, and its arm asks the host to play a sound by returning an inert PlaySfx("reset") command. Nothing here reaches out and does anything — the program only ever describes what should happen next.

Both entries in that capability list are load-bearing, and the second one is easy to forget. Drop sfx and the program stops compiling — not at the moment the sound would have played, but at the Reset arm, because emitting a command the manifest does not grant is [ErrCapDenied]. The list is not documentation of intent; it is the grant the compiler checks every cmds: against.

The five member names are fixed keywords, not identifiers you choose. Because the roles of the harness are part of the language, the compiler can check them:

The rest of this chapter takes those members one at a time, and then shows what the single journal underneath them buys you.

#The Model — bounded state

Every field of a Model must have a bounded kind. Scalars qualify; so do string (immutable UTF-8 with a declared cap) and decimal(scale); so do records and vec(κ, N) with a const-folded N. An unbounded field is [ErrState] — the Model’s exact analogue of the scene budget’s [ErrPlot]:

variant Verdict { Right | Wrong }

record Model { n: num ; label: string ; history: vec(Verdict, 64) }   // bounded — ok
// a growing list with no declared cap is not a Model field: ✗ [ErrState]

The cap is a const-folded length — a literal like 64, or an identifier that const-folds to one (vec(Level, MAX_LEVELS)). Either way the compiler knows the number before the first message arrives.

Why bound the Model. Because the memory footprint of an application then becomes computable at compile time. A running application cannot leak, thrash, or be killed mid-frame for exceeding a budget it never declared. Boundedness is not a restriction imposed on the author; it is what lets the compiler promise the budget in the first place.

#The doc / ui partition

One split is worth drawing from the first line, because every application with an undo needs it: put the business state — the state history owns — in a doc sub-record, and put the ephemera — the selection, the cursor, a half-drawn shape, an in-flight request’s epoch — in a ui sub-record that does not enter history. Without the boundary, undoing a change would resurrect a stale selection or a dead draft. With it, undo is exactly “truncate the journal to the previous bound and re-fold” — and we will return to why that matters.

You rewrite a model field with functional update: m with { … } rewrites the listed fields and carries the rest forward. It is shape-preserving — a field that does not exist is [ErrField], and a field you forget is kept, not silently lost:

update(m, msg) = match msg {
  Score(pts) -> { model: m with { doc: m.doc with { score: m.doc.score + pts } }, cmds: [] }
  Select(h)  -> { model: m with { ui:  m.ui  with { sel: h } },                   cmds: [] }
}

#A bounded collection you can add to and remove from

Editors keep drawings; a blotter keeps positions; a tool keeps anchors. All three want a collection you can add to, remove from, and address stably — yet the Model may not grow, may not re-index, and has no filter. The official pattern is a slotmap over a bounded vector: removal writes a tombstone instead of compacting, so nothing ever moves and every handle stays valid.

Figure — removal writes a tombstone; nothing ever moves, so every handle stays valid and the memory plan stays flat.

record Level { id: num ; price: price ; kind: Tool ; label: string ; gen: num }

record Model {
  slots:  vec(Level, MAX_LEVELS)   // a tombstone (`na`) marks a free slot
  live:   vec(signal, MAX_LEVELS)  // 1 where a slot is occupied
  count:  num
  nextId: num                      // the monotone domain-id counter (persisted)
}

// removal — functional, length-preserving, nothing shifts
def remove(m, h) =
  m with { slots: vec.setAt(m.slots, h.slot, na),
           live:  vec.setAt(m.live,  h.slot, 0),
           count: m.count - 1 }

// iteration — `na`-aware: a tombstone produces no child at all
view(m) = col { for lvl in vec.mask(m.slots, m.live) -> levelRow(lvl) }

Two guards make it correct rather than nearly correct: identity is dual — a stable domain id rides in the journal, undo and serialization, while the slot/generation handle stays an internal index rebuilt on load — and a generation counter defeats the classic ABA bug, so a stale handle reads na rather than a reused slot’s new item. The full four rules and the load-time clamp on nextId are the reference’s to hold; see The slotmap pattern →.

#update — pure, total, deterministic

update may not read the clock, may not read randomness, may not touch the DOM, may not read a live series inline. Everything ambient arrives as a message, and update must handle every one — match exhaustiveness is [ErrTotalMatch], checked, not hoped for.

It returns a named record, never an anonymous pair: { model: …, cmds: [ … ] }. And cmds is an ordered list of inert descriptors. A command is data — a sound’s name, a key, a score. It never carries a socket, a token, a URL, or a DOM handle: the host owns the resource, the script holds only a request.

#Asynchronous results come back as messages

The rule “everything ambient arrives as a message” holds even for the answer to a network request. A command that has a result carries the constructor its result should be wrapped in; the host applies that constructor to the outcome and delivers it back as an ordinary message:

variant Msg { Save | Saved(epoch: num, ok: signal) | Cancel }

update(m, msg) = match msg {
  Save        -> { model: m with { ui: m.ui with { epoch: m.ui.epoch + 1 } },
                   cmds:  [ SaveLevel(m.doc, m.ui.epoch + 1, Saved) ] }   // ← carries `Saved`

  Saved(e, ok) -> if e == m.ui.epoch                      // a stale result is ignored
                    then { model: m with { ui: m.ui with { saving: 0 } }, cmds: [] }
                    else { model: m, cmds: [] }
}

The epoch token there is the general answer to a stale result: the command carries an app-supplied scalar, the host echoes it back verbatim, and the arm compares it with the current epoch and drops what no longer matters. It lives in ui, never in doc — a stale-result guard must not travel into a shared journal.

Why not a composable Task type. An effect type that chained A ⤳ B(A) ⤳ C would hide the intermediate results — they would never reach the journal, and re-folding, time-travel and server-side replay would all lose the ability to reconstruct the model bit-for-bit. So every asynchronous result stays a message. The verbosity of a long chain is the acknowledged price of exact replay.

#view — a pure tree of vetted primitives

view returns a UiTree: containers (col, row, grid, stack, tabs, scroll, panel), content (text, label, badge, chip, icon, progress, sparkline, image), controls (button, toggle, slider, select, textInput, metaForm), and windows onto the other planes — chartView, paneView, sceneView. There is no raw markup, no HTML string, and no event handler. A click is a message:

view(m) = panel(slot: right.panel) {
  row { text("levels: {m.doc.count}") ; button("add", AddLevel) }
  chartView(chartId: "main",
            onClick: ClickAt,                       // a constructor reference, not a closure
            overlay: overlayOf(m.doc, m.ui.draft, m.ui.sel))
  when m.ui.saving: progress("saving…")
}

Two details in that snippet are load-bearing. Callback slots take a constructor reference, never a function. onClick: ClickAt names the constructor the host will apply to the real (bar, price) at the moment of the click, and the compiler checks that constructor’s payload kinds against the slot. No function value ever enters the lattice — there is no arrow sort, and this keeps it that way. And the chart is not re-rendered by the view diff: chartView mounts the real chart engine, and the reconciler only ever touches the chrome around it. The scene you pass as overlay: is a CANVAS value (scene{…}) — the sanctioned channel from the presentation plane into a pane, exactly the value you built in Guide §9.

The host diffs the small tree, sanitizes it — text goes in as text, an unknown node is rejected — and paints the whole view as an island: a <div> the real engine renders inside an ordinary static HTML page. This is why the plane’s rendering is safe: scene graphics and text inside a window both render on WebGPU, which sidesteps the DOM layout cost of moving many elements per frame — text as SDF glyphs, crisp at any zoom. chartView, paneView and sceneView are the sanctioned windows from the other planes into that island, and the chrome around them — a button, a panel, a row — takes its look from a closed set of typed style props the host validates and applies, never a raw CSS string. A view can therefore never inject markup, and a hostile application cannot draw a fake system dialog: the primitive set is closed, and the one injection surface a UI language usually exposes is structurally absent.

#subs — the declarative front door

Subscriptions are recomputed from each model, and the catalogue is closed. Everything ambient — time, input, randomness, data, the network, the wallet, other users — enters through it, as a message. Each subscription with a payload carries the constructor the host will apply, exactly as commands do (OnTick(100, Tick), OnSeries("rsi", Got)), and each is backed by a capability — OnSeries needs chart:read, OnFeed needs net:fetch, and so on. A handful of representative entries:

You compose them into a list, and — because subs is recomputed from the model — you can turn one on or off from state, and rate-shape it without leaving the model:

subs(m) = [ if m.ui.live then OnSeries("close", Got).throttle(100) else NoSub,
            OnChartClick(ClickAt) ]

The throttled edge is still journaled, so replay stays exact. The full catalogue — including the server plane’s OnWebhook / OnJob / OnQueue, delivered to a headless application with no viewport at all — is the reference’s to own; see The subscription front door → and server. A headless application is not a different kind of program: it is the same init/update/view/subs with a different set of inputs reaching it.

#Undo, redo and time travel come free

Now the payoff. In most codebases undo/redo is a feature you rebuild in every application — a stack of inverse operations, maintained by hand, and subtly wrong at the edges. In Flux you do not build it at all, because an application’s state never changes except through one journaled reducer. The model is a fold: fold(init, [the journal of every message so far]). Undo rewinds the journal one step and folds again; redo re-extends it. The state you land on is exactly the one you left — reproduced, not reconstructed.

variant Msg { Bump | Undo | Redo }

app tally {
  capabilities: [ journal ]

  init(p)        = { doc: { n: 0 }, ui: { pending: na } }
  update(m, msg) = match msg {
                     Bump -> { model: m with { doc: m.doc with { n: m.doc.n + 1 } }, cmds: [] }
                     Undo -> { model: m, cmds: [ Journal(UndoToMark) ] }
                     Redo -> { model: m, cmds: [ Journal(RedoToMark) ] }
                   }
  view(m)        = row {
                     button("undo", Undo)
                     text("{m.doc.n}")
                     button("+1", Bump)
                     button("redo", Redo)
                   }
  subs(m)        = []
}

The two arms that give this application its entire undo history return the model unchanged and hand the host an inert command. The host — which is where the journal lives — truncates it to the target and re-folds into the new model. Nothing in the application code knows how to reverse an edit; it only knows how to move forward.

One mechanism, two faces. For the user, this is undo/redo inside the app — an undo that cannot silently forget a field or resurrect a stale selection, in a level editor, a trading tool, a game. For the developer, the same journal is a time-travel debugger: the cursor of the analysis debugger becomes an event cursor. Scrub to any past message, step backwards, set a data breakpoint — stop at the first message where score crosses 100 — and put the run beside a reference run to see where they diverge. It falls out the same way for a level editor (every stroke is a message, so undo brings the drawing back exactly), a game (rewind to any move and replay from there — the match is the list of moves) and a blotter (scrub the position history like video, because the history is the journal).

Why undo is correct, and redo is exact. The doc/ui partition is what makes undo correct: it rewinds doc and leaves ui untouched, so it never revives a selection you made three edits ago. And because Flux is deterministic to the byte, re-folding the journal reproduces the state byte-for-byte — including the answers that came back from the network. An async result entered the model as a message, so it is already in the journal, replayed verbatim rather than re-fetched; rewinding never fires the request a second time.

Undo is free of bespoke work, not free of cost: it rebuilds the model by re-folding from the nearest memoized checkpoint, so it costs work proportional to the distance back to that checkpoint. The machinery — a journal, a fold, an event timeline — is real, modest, and reused by every application rather than rebuilt in each, which is the whole point. And note the exact claim: this is undo/redo over an application’s execution — the events it processed — never over its source code.

#Capabilities — the security model

The script never holds a capability object. It emits a request — emit Cap(args) — and the host, the only holder, interprets it through a handler only the host has. A request for a capability the manifest does not grant is rejected at compile time ([ErrCapDenied]), not at runtime. There is no ambient authority: no global object is in scope at all. Every grant is default-deny, host-attenuated, and graded by trust — net:fetch(domain) asks the user’s consent per domain and decodes the payload against the schema the app declared; storage:own gives a partitioned namespace with a quota; journal grants exactly the UndoToMark/RedoToMark truncate-and-re-fold you just saw.

Some things are inexpressible for every tier, trusted or not: eval and code generation, raw DOM, a raw socket, a raw database client, a token or a cookie, and any global store. They are not “forbidden by policy” — they have no name in the language.

Security is the grant, not the code. The first-party interface and a stranger’s application run the same language in the same sandbox; they differ only in what has been granted to them. A first-party module is trusted by perimeter — its source stays private, it ships as WASM, and its privileged grants sit behind an authenticated, admin-gated barrier. A marketplace application is untrusted from the point of view of whoever loads it: strict default-deny, sanitized view, isolated realm, and the buyer receives the WASM alone, never the source. Consent therefore cannot rest on reading the code — it rests on the sealed manifest, which travels with the binary, is derived by the compiler from the emit Cap sites, and is inspectable before install. This is precisely why the model holds for an author you cannot vet by hand — a marketplace developer, or a code generator: the guarantees are enforced by the grant and the sandbox, identically, whoever or whatever wrote the source.

Three more properties round out the model, each stated fully on the reference page: a dependency’s requests surface in the buyer’s manifest before install (authority flows only along import edges, never re-delegated), a grant can be revoked mid-session (journaled as CapRevoked, so commands fail closed and a re-fold reproduces it deterministically), and a module cannot declare itself trusted (trust is a server-side provenance record keyed by the binary’s content hash, not embedded metadata). See Capabilities — the security model → and host services.

#Testing an application

Because update and view are pure, total and deterministic, and the whole fold sits inside the byte-identity oracle, an application test is a golden over pure functions — with no mocks anywhere. The trace grain carries the weight, because the replay harness is the test harness: a trace test folds a literal message list and goldens the model it lands on. Nothing drives a live subscription, and nothing needs to — the journal already reifies every event as a message, so the message list is the mock:

// step — a deep, na-aware equality on two lattice values
assert update(m0, Tick) == { model: m0 with { n: 1 }, cmds: [] }

// view — a snapshot of the canonical view buffer
assert view(m1) == expectedTree      // chartView nodes are goldened as nodes, never as pixels

// property — an invariant asserted at every intermediate model, over a seeded message list
assert m.count == popcount(m.live)

The cmds field is inert data, so asserting which effects were emitted needs no fake clock and no fake socket: the descriptor is the assertion. A non-deterministic subscription is never mocked — it is goldened on its description (subs(m)), while its delivery is supplied as a literal list of messages. And where an invariant is already proven by the kind, no test is owed at all. Note the comment on the view line: a chartView node is goldened as a node, never as pixels — the test asserts the same numbers and the same scene on every machine, not the same pixels across GPUs.

#What replay proves — and what it does not

Server-side replay is the same idea aimed at trust rather than testing. Because a verdict is a pure function of (init, [msg]), a server can recompute it on the same bytes, and a claimed score that was not earned is a journal that does not fold to the claimed result. That property was inherited from determinism, not designed — and it comes with a precise limit worth stating plainly rather than as a slogan:

Replay proves the COHERENCE of a journal, not its NON-FALSIFIABILITY.

Figure — the journal is the single source of truth: undo truncates to a bound and re-folds; a checkpoint keeps that cheap.

“Diverges ⇒ tampered” is complete for a score derived from the seed and the elapsed time, because the server owns both — the seed is derived server-side and never accepted from the client, and the elapsed time of a ranked run is host-stamped and substituted at re-fold, so a forged Tick count buys nothing. It is not complete for one class, and the gap is open by name: a score fed by a host-pushed outcome — an OnReveal result the host computed — enters the journal as data, and a re-fold replays data verbatim. A forged outcome therefore re-folds to the claimed result without a whisper of divergence: the check passes; the claim is still a lie. The same class covers a pixel, which is derived from the client’s viewport and cannot be re-derived by a server that has none — hence the standing rule that a pixel value never feeds a ranked verdict.

An outcome-fed run therefore has exactly two honest destinations, and no third: the host re-derives the outcome server-side, or the run is local-score-only, excluded from the shared leaderboard. It is never accepted on the strength of the client’s journal alone. Guide §11 and server carry the closing argument; the mechanics — undo bounds, checkpoints, and the two host-mediated ways a model is ever produced outside update — are on the reference page’s Totality, determinism, replay →.

#Where the plane sits in the firewall

The APP plane is the most permissive of the four, and its permissions run one way. It reads analysis, read-only, through Sub OnSeries; it orchestrates the CANVAS and TRANSITION planes through commands; and it never writes analysis at all. So a game that switches asset does not repaint the indicator beside it — it recomputes it, through a capability — and scoring a quiz cannot repaint the indicator either. Reading a live series from update obeys the same floor-containing rule as any resample: the most recent closed unit — the bar, in charting — never a nearest match.

This is also where the honest shape of “total” shows through. update is total and its cost per message is bounded — heavy work is a command, outside the reducer, and the view diff touches a small tree. The language is deliberately not Turing-complete: it is total, bounded per step and unbounded over time, which is precisely what you want in a client-side reactive loop, where an unbounded inner loop is not a feature but a hung tab. You give up nothing you would have used, and you gain a memory footprint the compiler can promise before the first message arrives.

#A complete small app

The same handful of parts composes past a counter. Tic-tac-toe is the whole plane on one screen — a bounded Model, a total update a bad tap can only no-op, a view that is a pure function of the board, and not one effect or line of imperative state:

variant Mark { Empty | X | O }
variant Msg  { Tap(i: num) | Reset }

app tictactoe {
  capabilities: [ ]                          // pure: no clock, no chart, no effects

  init(_)        = { board: vec.fill(9, Empty), turn: X }
  update(m, msg) = match msg {
    Tap(i) -> if m.board[i] == Empty
              then { model: m with { board: m.board.set(i, m.turn), turn: other(m.turn) }, cmds: [] }
              else { model: m, cmds: [] }      // an occupied cell is a no-op, by construction
    Reset  -> { model: init(na), cmds: [] }
  }
  view(m)        = col {
    text("{glyph(m.turn)} to move")
    for i in vec.indices(m.board) -> button(glyph(m.board[i]), Tap(i))
    button("new game", Reset)
  }
  subs(_)        = [ ]
}

def other(t) = match t { X -> O   O -> X   Empty -> Empty }
def glyph(t) = match t { X -> "✕"   O -> "◯"   Empty -> "·" }

The APP plane that runs this is sealed design: the ANALYSIS-plane demos elsewhere on this site compile and render live in your browser today, while a playable board like this arrives with the app runtime. The shape, though, is exactly what you have been reading — nothing above is a construct the earlier sections did not name.

#See also

• Guide §9 — A scene that moves — the CANVAS scenes an application hands to a chartView as overlay:.
• Guide §11 — Determinism, replay, trust — the journal turned into a trust argument, and where a client’s word is not enough.
• Spec — the APP plane — the reference semantics of everything narrated here.
• Spec — Kinds — variant, record, and the bounded kinds a Model may hold.
• FDK — display — the view primitives, the scene value, panes and windows.
• FDK — server — headless applications, shared storage, and server-side replay.

The formal rules →

Everything this chapter narrated is specified exactly in the APP plane reference:

• What an application is — model, update, view, subs →
• The Model and its bounded kinds; the doc/ui partition →
• The slotmap, generation counters, and the load-time id clamp →
• update, asynchronous results, and the epoch token →
• view, the vetted primitives, and the plane windows →
• The closed subscription catalogue, including the server plane →
• Capabilities: default-deny, two trust tiers, transitive manifests, revocation →
• Totality, determinism, replay — and what replay does not prove →
• The byte-identity oracle behind exact replay →