Skip to content
Logo

Encapp for Elm developers

If you've built apps in Elm, you already understand the core of Encapp. The Elm Architecture (TEA) is a pure state machine — Model, Msg, update, view — and Encapp is exactly that, formalized in Lean. But Encapp diverges in one critical way: your app is not just runnable code, it is data, which means you can prove workflows rather than test them. This page maps what you know to what's new.

The Elm Architecture, abstract

In Elm, you write:

type Model = { … }
type Msg = ClickButton | Input String | …
update : Msg -> Model -> ( Model, Cmd Msg )
view : Model -> Html Msg

The runtime interprets Cmd Msg — it calls your HTTP handler, updates the DOM, fires subscriptions. The Cmd type is opaque; you do not control what the runtime does.

Encapp inverts that. The app is a pure data structure, and effects are data too:

structure App (Model Msg : Type) where
  init   : Model
  update : Msg → Model → Model × List Cmd
  view   : Model → View Msg
 
inductive Cmd where
  | submit : Event → Cmd
  | none    : Cmd

The Cmd is concrete: there are exactly two constructors. And the app is parametric — you give it to different interpreters (an emulator for proofs, a real adapter for deployment) and they behave the same by theorem.

Events, not HTTP

In Elm, Cmd is abstract, so you might emit Http.post, Task.perform, or Time.every. In Encapp, there is one Cmd: submit an Event to the store. An event is a fact:

structure Event where
  id   : String    -- unique, for idempotent replay
  data : String    -- opaque payload

Your app does not make HTTP calls or write files. It describes an event that the host should store. The host — a deployment using your app — decides whether "store this event" means "send it to the server", "persist it locally", or "drop it". Your update function neither knows nor cares.

This is the seam: your app speaks store, the host speaks wire. And the seam is proven to be sound.

Proofs via native_decide

Here is where Elm and Encapp diverge decisively. In Elm, you test:

test "hello message appears" =
  init
    |> update (Input "hello")
    |> update Submit
    |> view
    |> Query.fromHtml
    |> Query.has [ text "hello" ]

It runs. It passes or fails. It does not guarantee anything about the shipped JavaScript.

In Encapp, you write a workflow — a sequence of interactions and checks — and you prove it:

theorem helloWorkflow_holds : helloWorkflow.holds helloApp = true := by native_decide

This theorem says: replaying this workflow through the reflected interpreter produces a state in which all the post-conditions hold. And the proof is by computation — the Lean kernel verifies it by actually running the interpreter. At lake build, not at runtime.

The reflected interpreter (reflStep) is the same one the emitted JavaScript uses — it is the operational mirror of the Lean semantics. So a workflow that is proven in Lean is proven to hold on the shipped JavaScript too, checked empirically against the emulator oracle.

The store, refined by theorem

In Elm, you trust the runtime. In Encapp, the host is proven to be correct.

An app's Cmd.submit goes to a World — an interpreter that runs the command and returns the committed events. There are two canonical worlds:

  1. The emulator: state is the event log itself. submit appends and returns the new event.
  2. The real adapter: state is whatever the host keeps (memory, a database, the wire). It also runs the command and returns the committed events.

The proof is called refines_sound:

If a World refines the emulator under some relation, then for every command sequence, the emitted event traces are equal and the final states stay related.

In other words: if your host's World is proven to refine the emulator, then running your app on the emulator is observationally identical to running it on the host. You get the emulator as a spec and a simulation theorem that says the real thing is equivalent.

theorem refines_sound {H : Type} (w : World H) (R : H → List Event → Prop)
    (hr : Refines w R) :
    ∀ (cs : List Cmd) (h : H) (s : List Event), R h s →
      (w.runAll cs h).2 = (emulator.runAll cs s).2
      ∧ R (w.runAll cs h).1 (emulator.runAll cs s).1

This is what Elm leaves to the runtime and the hope of testing. Encapp proves it.

Ports become host bindings

In Elm, a port is:

port updateProfile : Profile -> Cmd msg

You declare what the outside world should do. The JavaScript fills the other end. There is no enforcement — the host could ignore the port entirely and the app would have no way to know.

In Encapp, a host binding is a typed, declared contract. An app declares what it expects of its host:

structure SdkBinding where
  package : String
  submits : List (String × String)    -- table → SDK method
  deletes : List OpBinding            -- delete contracts

The emitted artifact carries the serialized binding. The host reads it and obeys it, or a test fails. The binding is not a comment; it is an executable constraint.

A test that exercises host behavior must load the emitted binding, not a hand-written stub. A stub is a fiction — the app and the test can disagree and nothing notices. This is not hypothetical; it happened in production audits. The framework now enforces: load the real binding or the test is unsound.

One interpreter per platform (not elm-make + js)

Elm has a beautiful property: elm-make produces JavaScript, and the JavaScript is the Elm. They are the same thing, differing only in syntax.

Encapp is different. There is a Lean interpreter (reflStep) that the proof tier uses, and there is a JavaScript interpreter that the browser/native runtime uses. They are operationally equivalent by construction — the JavaScript is a direct translation of the Lean — but they are not identical. This is why the empirical corpus matters. If they diverge, the corpus tests catch it across four runtimes.

A deployment also supplies its own World interpreter, which may handle the store differently (e.g., persisting to disk vs. an in-memory emulator). Again, proofs hold because of refines_sound, not because they are identical implementations.

What Elm devs will miss

Type-driven error messages

Elm's compiler is legendary for its error messages. Encapp's Lean compiler is not. You will get type errors, but they will be terse. The community has written high-quality linters; this repo does not bundle them.

Packages and the ecosystem

Elm's package manager is trustworthy. You can pull in a library with confidence that it will not have side effects or break your bundle size. Encapp is younger. The dependency graph is lean (Lean itself, a test harness, a handful of utilities), but do not expect the breadth of Elm's ecosystem.

Hot reload and fast iteration

Elm's dev experience is snappy: edit, save, live reload. Encapp's build is lake build, which compiles Lean proofs. The first build takes a minute; incremental builds take seconds. You lose the immediacy. Workflows and apps are tested via a replay corpus that runs on four runtimes and can take a few seconds per run.

What Elm devs gain

Proofs that workflows are correct

Every workflow in your test suite becomes a theorem. A divergence in the logic (or the interpreter) will cause lake build to fail. You do not have to choose between "test the proof tier" and "test the runtime" — both happen simultaneously, and if they diverge, the build catches it.

The store is proven

Your host's World is proven to refine the emulator. This is not a claim or a best-effort test; it is a closed simulation argument by induction on the command list. If the host diverges, the theorem fails to discharge and the build fails.

Apps are data

Because your app is a ReflApp — pure data, not code — it can be inspected, transformed, and combined without running it. The framework emits a SPA from it; it can also serialize the workflow corpus as JSON, run it on any platform, and prove cross-platform equivalence by replaying the same steps everywhere.

Recap

  • Model, Msg, update, view map 1:1 to Encapp's App structure — it is the Elm Architecture, formalized.
  • Effects are data. A Cmd is a submit : Event → Cmd or none. The app never performs I/O; it describes store writes.
  • Workflows become proofs. A test that is by native_decide is a theorem, checked at lake build time, over every workflow in your corpus.
  • The store is proven. A World that refines the emulator is proven by refines_sound to produce identical event traces and related final states for every command sequence.
  • Host bindings replace ports. Declarations are enforced by the emitted artifact and checked by the deletion test. An untyped extension point is an invitation to hand-write; a typed one is not.
  • The honest boundary: proofs hold for the Lean tier. The JavaScript is checked empirically against the emulator on four runtimes.

Next steps