Effect4 is Effect's runtime written in Lean as a model with defined semantics. A program is data: a typed term that Lean checks, runs on a reference machine, lowers to OCaml and prints as TypeScript.
Each claim about that runtime carries its evidence: a theorem that is proved, a theorem proved modulo named goals, or a planned goal stated with its proof to come.
Start here#
- Semantics evidence: every claim by concept, its status and its Lean statement, and the plan of goals that the open requirements rest on.
- Document specimen: every kind of block and status mark, as the pages draw them.
For a framework#
Every page is also its document as JSON, in the format effect4-document/1: the semantics page and the specimen. The report behind the semantics page is report.json.