Skip to content
Logo

Web

Emitting

def main : IO Unit := do
  let html := AppGen.emit (DocChrome.light "Hello") helloReflected
  IO.FS.createDirAll "dist"
  IO.FS.writeFile "dist/index.html" html
~/.elan/bin/lake exe helloapp
open dist/index.html

One file. No build step, no bundler, no node_modules, no framework dependency at runtime. Opening the file directly works — there is nothing to serve.

What is in the file

<!doctype html>
<html><head>
  <title>…</title>          ← DocChrome.title
  …                          ← DocChrome.head   (extra <head> lines, e.g. fonts)
  <style> … </style>         ← DocChrome.css
</head><body>
  <div id="app"></div>
  <script>
    const APP = { init, pages, handlers, gates, binding };   ← the serialized ReflApp
    …appCoreJs…              ← the state machine
    …appDomJs…               ← the DOM renderer
  </script>
</body></html>

Chrome is data

structure DocChrome where
  title : String
  head  : String := ""    -- extra <head> lines
  css   : String          -- the <style> body

This is what keeps the emitter generic: one AppGen.emit serves every app, and presentation is the app's own value rather than a per-app emitter function. DocChrome.light is the default theme used by the examples — a light colour scheme, a 520px centred column, and sane defaults for inputs and buttons.

For a product with its own design system, pass your own DocChrome and author screens with the styled view vocabulary so the entire UI, chrome included, is view data.

The runtime, in two halves

def appRuntimeJs : String := appCoreJs ++ "\n" ++ appDomJs

appCoreJs is the state machine — the live Doc in S, step(tag, payload), the Eff interpreter, gate evaluation and path routing. It is the operational mirror of reflStep, and it is shared verbatim with the native target.

appDomJs is the renderer — each RView constructor to a DOM node, event wiring to step, input binding, and browser history.

The split is the reason a logic change cannot make web and native diverge: there is one logic artifact and two renderers.

The runtime hook

window.__enc = { S, step, render }

S is the live Doc; step(tag, payload) dispatches a handler; render() repaints. Every replayer drives the app through this hook, which is why the same corpus runs unchanged on happy-dom, headless Chromium, React-Native-web and Electron.

It is also useful by hand — open the console on a built page and inspect __enc.S to see exactly the state your proofs talk about.

Routing and history

The current page is the path scalar. The runtime wires pushState on navigation and popstate for the Back button, so deep links resolve and history behaves. Gates are evaluated before the path lookup, so a guarded app cannot be entered by editing the URL.

Verification tiers

node test/encapp-replay-dom.mjs dist /tmp/corpus.json   # happy-dom, fast
node test/encapp-replay.mjs     dist /tmp/corpus.json   # headless Chromium

The dom tier is fast enough to run on every save; the hl tier catches anything that depends on real layout, real events or real history. Both execute the same emitted corpus and assert the same Doc post-conditions the proofs assert, plus the replay-only ui checks.

Serving

Static hosting is enough — any file server, any CDN, no server-side rendering and no runtime dependency. If your app declares a host binding, the deployment must also supply the adapter that satisfies it; that adapter is ordinary hand-written code and lives outside the proof boundary.

Recap

  • AppGen.emit produces a single self-contained HTML file with no build step or bundler
  • DocChrome structures the HTML head and styles as app data; emitter stays generic
  • The state machine (appCoreJs) is shared verbatim with native; only the renderer (appDomJs) differs
  • The runtime hook (window.__enc = { S, step, render }) exposes the live state machine
  • Routing uses path scalar with pushState/popstate; gates evaluated before path lookup
  • Verification spans happy-dom (fast), headless Chromium (real layout), and Electron tiers
  • Deployment requires only static hosting; host bindings need external adapter code

Next steps