Skip to content
Logo

Thinking in Encapp

Unlike React (where components hold local state and the framework reconciles trees) or vanilla Elm (where the app state is opaque), Encapp's mental model is: your app IS its state machine, and state IS data.

This page walks through the mental shift: starting from a tiny feed-and-composer UI, you'll model its state as a Doc, express its interactions as effects, and write workflows that are simultaneously proofs.

A tiny mockup: feed + composer

Imagine:

  • A feed that shows posted messages (sender, body, timestamp)
  • A composer below it (text input + Send button)
  • A Connect screen that appears when identity is empty (a guard)

That's your whole app. No state hidden in components. Everything lives in the Doc.

The Doc: state as data

A Doc is a plain value — scalars (strings, ints, bools, null) plus tables (lists of rows). Both are decidable, which means you can write a proof about them:

structure Doc where
  scalars : List (String × Atom)  -- "identity", "draft", "path", etc.
  tables  : List (String × List Row)  -- "messages", "peers", etc.

For the feed + composer, your init looks like:

def feedInit : Doc := {
  scalars := [
    ("identity", .null),      -- not connected yet
    ("draft", .str ""),        -- empty composer
    ("path", .str "/feed")
  ],
  tables := [
    ("messages", [])           -- no posts yet
  ]
}

Why scalars vs tables? Anything that appears in exactly one place is a scalar: the current user, the draft text, the active page. Anything that is a list of similar records is a table: messages, group members, notification history. The line is simple: if you'd write d.getScalar "identity", it's a scalar. If you'd write d.rows "messages", it's a table.

Interactions become handler tags

Every click, form submission, or navigation is a (tag, payload) pair. The tag names the intent ("submit", "delete:row"). The payload is either a scalar (a text field's value) or a row (when you select a row from a list):

inductive Payload where
  | atom : Atom → Payload   -- scalar payload (empty post → .null)
  | row  : Row → Payload    -- row payload (delete this message)

For the feed app, your handlers might be:

  • "connect" (tag) + a pubkey string (payload) → set identity and hide the guard
  • "draft" (tag) + the typed text (payload) → update the draft scalar
  • "submit" (tag) + .null (payload) → send the draft, clear it, add to feed

Effects express state changes

A handler is just a list of effects. Each effect is a language — not arbitrary mutations, but declared operations. The domain-free ones work for any app:

| setConst : String → Atom → Eff
| appendFromScalars : String → List (String × Atom) → List (String × String) → Eff
| removeWhereField : String → String → Eff

From Encapp/AppGen.lean, the full alphabet includes chat vocabulary too (setConvId, pushConvMessage), but start with the domain-free ones. Your feed app's "submit" handler:

{ tag := "submit",
  effs := [ .pushDraft "messages",       -- append the draft row to "messages"
            .setConst "draft" .null ] }  -- clear draft

pushDraft table appends the row built from the draft scalar to the named table. (pushInput is its payload-routed sibling: it takes no argument and reads the target table from the message payload.)

Pages and routing: path is a scalar

Navigation is not a separate concern. The path scalar holds the current page name ("/feed", "/connect"), and the view layer picks the page by reading that scalar. A handler navigates by setting path:

.setConst "path" (.str "/settings")

Route guards are explicit — if identity is empty, the view renders "/connect" regardless of what path says, checked once per render. This prevents skipping onboarding.

Write the workflow first

A Workflow is a sequence of user interactions plus checks about the state afterwards. The same definition is used two ways:

  1. Proof: by native_decide verifies it holds for your interpreter
  2. Test: The emitter turns it into JSON that replayers run on four runtimes (DOM, headless Chromium, React Native, and Electron)

Start with one user story: "A user connects and posts a message."

def feedPostWorkflow : Workflow where
  name := "post-after-connect"
  users := ["alice"]
  steps := [
    .fire "connect" (.atom (.str "79be667ef9dcbbac")),
    .input "draft" (.str "hello world"),
    .fire "submit" (.atom .null)
  ]
  checks := [
    .scalarEq "identity" (.str "79be667ef9dcbbac"),
    .scalarEq "draft" .null,
    .tableLen "messages" 1,
    .rowField "messages" 0 "body" (.str "hello world")
  ]
 
theorem feedPostWorkflow_holds :
    feedPostWorkflow.holds feedReflected = true := by native_decide

If your handler or interpreter doesn't match, the proof fails at lake build time. That's the contract. The emitted JSON from this workflow is also the test that replayers run:

{
  "name": "post-after-connect",
  "users": ["alice"],
  "steps": [
    {"as":"alice","do":"fire","tag":"connect","payload":"79be667ef9dcbbac"},
    {"as":"alice","do":"input","field":"draft","value":"hello world"},
    {"as":"alice","do":"fire","tag":"submit","payload":null}
  ],
  "checks": [
    {"kind":"scalar","key":"identity","eq":"79be667ef9dcbbac"},
    {"kind":"scalar","key":"draft","eq":null},
    {"kind":"tableLen","table":"messages","eq":1}
  ]
}

Making it hold: mental model vs React & Elm

vs React: React asks "what DOM should I render given the state?" and reconciles trees. Encapp asks "given the state, which page does the view deserialize?" There are no components with local state, no lifecycle hooks. The state machine is all there is. Every piece of state is in the Doc, visible and testable.

vs Elm: Elm has the same TEA shape (Model, Msg, Update), but in Elm the Model is opaque — you reason about it through its type. Encapp's Doc is concrete data, so the workflow's checks are decidable: your proof is the test. A proof that fails means your app disagrees with the proof, caught at compile time across all four runtimes simultaneously.

Recap

  • State is a Doc: scalars for singular values, tables for lists of records
  • Interactions are (tag, payload) pairs that fire handlers
  • Handlers apply a list of effects — operations on scalars and tables, not arbitrary mutations
  • Pages live in the Doc too (the path scalar) — no separate router
  • Write workflows first: they are simultaneously proofs and tests
  • native_decide makes it real: if the proof compiles, every runtime agrees

Next steps