Encapp for React developers

Coming from React, you'll find familiar patterns in Encapp — stateful components, event handlers, rendering — but they map to a fundamentally different architecture. This page lists the honest boundaries so you know what to expect.

From React component tree to Encapp pages and state

React: You build a tree of components, each with useState for local state and props from parents. React re-renders when state changes.

Encapp: The entire app state lives in one Doc — a map of named scalars (strings, numbers, booleans) and named tables (lists of rows). Each page is a View function that reads from this single source of truth.

-- Counter, React-style (pseudo-code)
function Counter() {
  const [count, setCount] = useState(0)
  return <button onClick={() => setCount(count + 1)}>+</button>
}
 
-- Counter, encapp-style (real code)
def counter : Spec where
  init   := [("count", 0)]
  view   := .col [ .button "-" "dec", .bind "count", .button "+" "inc" ]
  update := [ ⟨"inc", "count", .incr⟩, ⟨"dec", "count", .decr⟩ ]

The init field defines your scalars and tables. The view is a function that takes a Doc and returns a View — no component hierarchy, one deterministic render per state.

From setState to handlers and effects

React: setState merges new values into component state and triggers a re-render. Side effects live in useEffect.

Encapp: A handler is a tag (the message name) plus a list of Eff values — pure data describing state changes. When you click a button, it fires a handler tag; the handler runs its effects in order, each transforming the Doc. No re-render call; the runtime applies effects and renders the new state.

-- React (pseudo)
function Submit() {
  const [draft, setDraft] = useState("")
  const handleSubmit = () => {
    postMessage(draft)
    setDraft("")
  }
  return <button onClick={handleSubmit}>Send</button>
}
 
-- Encapp: the same flow as pure data (real code)
def helloHandlers : List RHandler :=
  [ ⟨"submit", [ .pushDraft "messages",          -- append the draft as a message row
                 .setConst "draft" .null ]⟩ ]   -- clear the draft scalar

Each Eff is one operation: setConst sets a scalar, appendFromScalars builds and appends a row, setInput sets a field from the message payload. They are applied left to right, so ordering matters — clear the draft after you consume it.

From props and state to scalars, tables, and payloads

React: Props flow down; state is co-located with a component.

Encapp: All state is visible to all handlers and views. You navigate the state tree explicitly:

• Scalars — atomic values. getScalar "path" reads the current route; setScalar "identity" (.str pubkey) sets the user identity.
• Tables — lists of rows. appendRow "messages" row adds a message; rows "messages" reads all messages.
• Payloads — what a handler receives from the message. A button click may carry a scalar (a user input) or a row (the entire message you clicked on).

def helloView (d : Doc) : View HMsg :=
  match asStr (d.getScalar "path") with
  | "/feed"  => .col [ .list "messages" (.rowField "body"),
                       .input "draft", .button "Post" .submit ]
  | "/about" => .text "About this app"
  | _        => .text ""

No props passed through a component tree — routing is a scalar like any other, and every view sees the whole Doc.

From JSX to View constructors

React: You write HTML-like JSX that compiles to React.createElement calls.

Encapp: You build View trees with constructors. The available tree nodes are simple and intentional:

That is the whole API. No conditional rendering (use match in Lean); no forms (build rows from scalars); no lifecycle. The View is a function; call it at the top level and it walks the current Doc deterministicallly.

Why there is no useEffect

React: useEffect runs side effects after render — fetching data, logging, subscriptions.

Encapp: There is no equivalent because effects are not for side effects. An Eff is a pure state transformation (setConst, appendFromScalars). Network calls, logging, and persistence are the host adapter's job, not the app's.

When you emit an app, the handler table includes a Cmd list — structured descriptions of what the host should do (store a message, upload a file, etc.). The adapter implements those Cmd handlers in JavaScript. That separation keeps the app provable.

def helloApp : App Doc HMsg where
  update msg d := match msg with
    | .submit =>
        let d' := (d.appendRow "messages" (postRow d)).setScalar "draft" .null
        (d', [ .submit { id := short16 (asStr (d.getScalar "identity")),
                        data := asStr (d.getScalar "draft") } ])
    -- ↑ The Cmd is returned; the host decides how to execute it.

The Lean app says what to store; the JavaScript adapter says how.

From tests to compile-time proofs

React: You write tests with Jest or Vitest that run assertions at build time or in CI.

Encapp: Tests are theorems checked at lake build. Define a Workflow — a sequence of user interactions and post-condition checks — and add by native_decide to prove it holds:

def helloWorkflow : Workflow where
  name   := "hello-post"
  steps  := [ .fire "connect" (.atom (.str "79be667ef9dcbbac")),
              .input "draft" (.str "hello from node:test"),
              .fire "submit" (.atom .null) ]
  checks := [ .tableLen "messages" 1,
              .rowField "messages" 0 "body" (.str "hello from node:test") ]
 
theorem helloWorkflow_holds : helloWorkflow.holds helloReflected = true := by native_decide

If the handler drifts, the proof fails to compile. That is stricter than a runtime assertion — it catches bugs before any code ships. The same workflow also runs as a cross-platform test corpus (DOM, Chromium, React-Native-web).

What codegen means (and what it does not)

React: Your JavaScript runs as written (minus minification).

Encapp: Your Lean app is compiled to two targets:

1. The Doc interpreter — JavaScript that replays a message sequence and emits the final state. This is embedded in the SPA and used for load/reload.
2. The handler table — a JSON description of effects, not functions. The emitted runtime walks this table and applies effects to the Doc in memory.

The codegen is not automatic code generation in the Babel sense. It is a deterministic translation from your reflected app (data) to HTML + runtime. The semantics are proven to match: if reflRun (the Lean interpreter) reaches state S, the JavaScript runtime will too.

This is why there is no imperative JavaScript in an Encapp app. The app is data; the runtime is the same for every app; bugs are in your handlers (which are data and therefore provable), not in shared runtime code.

What you will not have

Local component state

React's useState lets each component have private state. Encapp has one Doc for the whole app. You cannot hide state from other parts of the app, which eliminates a class of bugs but also means no private, transient component state. Work around it by using a scalar like "ui_draft" for transient editor state.

React ecosystem

No hooks (useContext, useCallback, etc.), no libraries (react-router, react-query, Zustand), no custom hooks. Your app is its own thing, proven in isolation. If you need a library's logic, translate it to a Lean function or an effect.

JavaScript interop

You cannot call arbitrary JavaScript from an Lean app. Handlers are pure effects; views are pure functions. If you need interop (a native module, a third-party API, a browser API), that logic lives in the host adapter, and you call it via a Cmd.

Development patterns

No hot-module reloading, no browser devtools for React. lake build compiles your app; if it fails, you see a Lean error, not a runtime crash. There is no "develop in the browser" — develop in your editor, compile, verify proofs, run the corpus tests locally.

Mental model shift

The biggest shift: state is not a property of components; it is the single truth about your app. Handlers do not return new JSX; they return new state. Views do not cache computed state in useMemo; they compute it deterministically from the current Doc every time. Tests do not mock; they replay real message sequences.

This constraints your design space. But it also means your app's behavior is decidable — you can reason about it mathematically, test it at compile time, and prove it correct.

Recap

• Component tree → one Doc source of truth + one View function per page
• setState → handler effects applied left to right
• props/state → scalars, tables, payloads read from the Doc
• JSX → View constructors (simple, intentional set)
• useEffect → host adapter's Cmd handlers
• Tests → Workflow proofs checked at lake build
• Codegen → deterministic translation of data to HTML + runtime
• You lose component encapsulation, the React ecosystem, and imperative JavaScript; you gain proofs and a single determinate state model

Next steps

• Read The app model for a complete walkthrough of the hello example (state, view, update, reflection, proof).
• See Effects for the full Eff algebra and when to use domain-free effects vs. chat-shaped conveniences.
• Check Workflows and proofs to learn how to write tests that compile.