The thesis

TEA and the enc store are the same machine

The Elm Architecture gives the clean skeleton: update : Msg → Model → (Model, Cmd), effects-as-data, view : Model → View Msg. What TEA leaves implicit is the runtime — the thing that interprets Cmd. In practice that runtime is where correctness goes to die, because it is hand-written, untyped, and unproven.

Encapp makes the runtime a first-class object and proves the three properties TEA only assumes:

structure World (H : Type) where
  empty : H
  run   : Cmd → H → H × List Event   -- interpret one command
  log   : H → List Event             -- the observable committed log

The emulator is the denotational spec — its state is the event log. A real backend is any other World that refines it. refines_sound then proves, by induction on the command list, that a refining world emits byte-identical event traces for every command sequence.

That theorem is the pure form of the "in-memory mode ≡ real backend mode" claim that most frameworks state in a README and never discharge.

An app has to be data before it can be proven

The abstract App Model Msg has function fields. Functions cannot be serialized, cannot be walked by a code generator, and cannot be compared by decide. So Encapp keeps two faces of the same app and ties them together:

The reflected form is a defunctionalization: messages become string tags, update becomes a finite handler table, and the view becomes a finite tree. Encapp/Examples/Hello.lean carries both and ties them with a theorem (hello_reflected_matches), so the ergonomic face and the compilable face cannot drift.

Once the app is data:

• Proofs become computation. Workflow.holds app w is a Bool, so a whole user story is discharged by native_decide at build time.
• Codegen cannot fail. There is no code to generate — there is a value to serialize, and one generic interpreter per platform that already exists and is already tested.
• Platform drift becomes structurally impossible. Web and native share the emitted appCoreJs verbatim; a checked gate asserts they are byte-identical. Desktop reuses the web artifact whole.

One interpreter per platform, not one per app

The usual multi-platform story is "write once, generate three codebases", and the failure mode is that the three generated codebases drift and each needs its own tests.

Encapp inverts it. The app is data that never changes shape across platforms; what differs is the interpreter, and there is exactly one per platform:

        the app (data, proven)
                 │
    ┌────────────┼────────────┐
appDomJs     appRnJs      (web emit)
  web        native        desktop

All three consume the same appCoreJs state machine. So a bug in app logic is one bug in one place, and a workflow proven once is meaningful on every tier.

Effects are the seam, and the seam is typed

An app cannot perform I/O. It can only describe a store write. What runs those descriptions is chosen downstream and is related to the spec by proof.

The same discipline applies to what an app expects from its host. The HostBinding typeclass is deliberately opaque: Encapp knows a binding can be serialized and nothing else. Anything protocol-shaped — SDK packages, enclaves, plugins — is defined by the layer above and passed in as a type parameter, so the dependency arrow points one way. Generators may depend on this vocabulary; this vocabulary never depends on a protocol.

That existed for a concrete reason, recorded in the source: the store-write seam used to be an ambient, untyped hole (window.ENC_ADAPTER). Nothing declared what a deployment owed the app, so a hand-written protocol implementation could fill it and pass every UI check. An untyped extension point is an invitation to hand-write protocol; a typed, declared one is not.

What this buys, stated plainly

• A user story that is proven, not tested, and fails the build when logic drifts.
• A backend swap that is proven not to change behaviour, rather than hoped.
• Three platforms whose logic cannot diverge, because there is only one logic artifact.

For the limits of these claims — and there are real ones — read What is proven (and what is not).