Skip to content
Logo

Tutorial: build Hello (part 1)

This tutorial walks you through rebuilding the Hello app—the Encapp showcase—from typed logic to shipped code. You'll see how three layers connect: a typed message algebra, a routed view, and the reflection to codegen-ready data. By the end, your app compiles, every theorem checks, and part 2 ships it.

Step 1: Define typed messages

The first thing an Encapp does is make routing a type. In a traditional SPA, a click fires a string; in Encapp, it fires a constructor. That makes typos impossible.

inductive HMsg where
  | connect : String → HMsg     -- wallet pubkey
  | input   : String → HMsg     -- new draft value
  | submit  : HMsg              -- post the draft
  | nav     : String → HMsg     -- route to a path
  deriving DecidableEq, Inhabited

Why this first? A typed message union is the contract between the view and the logic. Every interaction flows through it, so typos in handler names stop the build. The deriving attributes make it decidable—necessary for theorems that need to reason about message equality.

Step 2: Define the initial state

The state is a Doc—a schema-validated union of scalars (strings, nulls, numbers) and tables (lists of rows). Here we define three scalars (identity, path, draft) and two message tables:

def helloInit : Doc where
  scalars := [ ("identity", .null), ("path", .str "/connect"), ("draft", .str "") ]
  tables  := [ ("messages", []), ("my_messages", []) ]

Why Doc? It is observable—JSON-serializable and queryable without heap inspection. Every state the app reaches can be tested, diffed, and replayed on any runtime without special hooks. The schema is implicit in how you name and type the scalars and rows.

Step 3: Write the routed view

The view is a function from state to View HMsg. It pattern-matches on the path scalar to decide which screen to render. Each screen is built from primitives: text, buttons, input fields, and lists that bind a table into DOM.

def helloView (d : Doc) : View HMsg :=
  match asStr (d.getScalar "path") with
  | "/connect"  => .col [ .text "Connect your wallet to use Hello.",
                          .button "Connect" (.connect "79be667ef9dcbbac") ]
  | "/feed"     => .col [ .list "messages" (.rowField "body"),
                          .input "draft", .button "Post" .submit,
                          .button "My posts →" (.nav "/my_posts") ]
  | "/my_posts" => .col [ .list "my_messages" (.rowField "body"),
                          .input "draft", .button "Post" .submit,
                          .button "← Feed" (.nav "/feed") ]
  | _           => .text ""

Why this style? Routing is plain logic—no JSX, no URL parsing library. The view is total: unmatched paths go to empty, and the compiler will warn you if you forget a case. The .list "messages" (.rowField "body") line binds the table to the DOM; theorems later verify the right table is bound to each page.

Step 4: Write the update logic

The App ties state, messages, and view together. The update function takes a message and current state, and returns a new state plus a list of effects (things to send to the backend):

def helloApp : App Doc HMsg where
  init := helloInit
  update msg d := match msg with
    | .connect w => ((d.setScalar "identity" (.str w)).setScalar "path" (.str "/feed"), [])
    | .input v   => (d.setScalar "draft" (.str v), [])
    | .submit    =>
        let d' := ((d.appendRow "messages" (postRow d)).appendRow "my_messages" (postRow d)).setScalar "draft" .null
        (d', [ .submit { id := short16 (asStr (d.getScalar "identity")), data := asStr (d.getScalar "draft") } ])
    | .nav p     => (d.setScalar "path" (.str p), [])
  view := helloView

Why separate state from effects? The logic is deterministic: the same message replayed twice reaches the same state. Effects (the .submit { … } return) are separate and declarative—they tell the backend what happened, but do not affect the proof. If an effect call fails, the app state does not rewind; it stays committed. This is the boundary between the app's logic (proven) and the backend (trusted but not proven).

Step 5: Reflect to the codegen-ready layer

The typed App is not what the emitted runtime sees. Instead, you reflect it to a ReflApp, which the emitter serializes to JSON and JavaScript. This step defunctionalizes messages and views:

def encodeMsg : HMsg → String × Atom
  | .connect w => ("connect", .str w)
  | .input v   => ("set:draft", .str v)
  | .submit    => ("submit", .null)
  | .nav p     => ("nav", .str p)

Then build a handler table that mirrors the update logic, but in declarative form:

def helloHandlers : List RHandler :=
  [ ⟨"connect",   [ .setInput "identity", .setConst "path" (.str "/feed") ]⟩,
    ⟨"set:draft", [ .setInput "draft" ]⟩,
    ⟨"submit",    [ .pushDraft "messages", .pushDraft "my_messages", .setConst "draft" .null ]⟩,
    ⟨"nav",       [ .setInput "path" ]⟩ ]

And render every routable page:

def helloPages : List (String × RView) :=
  ["/connect", "/feed", "/my_posts"].map
    (fun p => (p, reflectView (helloView (helloInit.setScalar "path" (.str p)))))
 
def helloReflected : ReflApp Unit where
  init     := helloInit
  pages    := helloPages
  handlers := helloHandlers

Why this two-stage process? The typed version is readable and reasoned about; the reflected version is what the runtime executes. By proving they match, you get both the clarity of types and the speed of a compiled interpreter—on web, native, and node.

Step 6: Prove the reflected app matches the typed one

Now the centerpiece: a single theorem that asserts the codegen'd app (which the deployed runtime runs) reaches the exact same state as the proven typed app:

def demo : List HMsg :=
  [ .connect "79be667ef9dcbbac", .input "hello from node:test", .submit ]
 
def helloFinal : Doc := helloApp.ofMsgLog demo
 
def demoSteps : List (String × Payload) :=
  [ ("connect", .atom (.str "79be667ef9dcbbac")), 
    ("set:draft", .atom (.str "hello from node:test")), 
    ("submit", .atom .null) ]
 
theorem hello_reflected_matches : reflRun helloHandlers demoSteps helloInit = helloFinal := by
  native_decide

The native_decide tactic compiles both the typed interpreter and the reflected interpreter to Lean bytecode, runs them both, and verifies the final states are byte-identical. This theorem holds for every app on the framework—the proof does not assume anything about what messages or tables you choose. Shipped with the proof are extra theorems that lock down individual postconditions (draft is cleared, one message exists, the body is correct).

Recap

  • Typed messages are your API contract—a union that prevents routing typos.
  • Doc state is observable and testable, not hidden in heap objects.
  • View functions pattern-match on state to produce DOM; routing is logic, not magic.
  • App.update is pure: same message, same state transformation, always.
  • Reflection bridges the typed world and the runtime—one theorem proves they stay in sync.
  • native_decide runs on web, native, and node, proving the claim holds on all platforms.

Next steps