Where the ideas come from

The languages, systems and papers Lema builds on, what it takes from each, and where it departs from them.

Most of Lema’s design is borrowed. This page names the sources, says what Lema takes from each, and says where it does something different. For the reasoning behind particular choices, see Design decisions.

Lean and Mathlib

Lean is a proof assistant built on a dependent type theory. Its elaborator and tactic framework are large, and its kernel, which checks the proof terms they produce, is small. Lema uses Lean as its only proof checker. Every acceptance is a replay through the pinned Lean 4.34.1 kernel, and authors write restricted Lean. The project will not build a separate production checker without a concrete, diagnosed reason.

Mathlib, Lean’s community library of mathematics, shows that a library of checked results can grow very large by proving new theorems from old ones. Lema wants that kind of cumulative growth for software (Build software like mathematics).

Lema departs from both in how code is kept. A Lean project is a tree of source files and modules addressed by name, and editing a file means rebuilding what imports it. A Lema store keeps elaborated kernel terms as objects identified by hash, and accepts them by replaying those objects with no source. The exporter refuses any external constant from outside Lean’s Init, so Lema code cannot use Mathlib today (authoring rules).

Unison

Unison identifies each definition by a hash of its syntax tree. It keeps code in a database instead of text files, and it stores names separately from definitions, so renaming a definition does not break its callers. Lema takes all three ideas. Objects are identified by the SHA-256 of their canonical form, names are aliases kept outside identity, and source files are views (Code stored by identity).

The differences come from proofs. Lema hashes the elaborated kernel term instead of the source syntax, and it splits each declaration into a statement, a template and proof objects. Theorems are cited by their statement and definitions by their template, so a proof can change without changing the objects that cite it. Unison has no proofs, so it has no reason to make that split. Lema also cites Lean’s own Init constants by name, and a namespace object pins the Lean version and source revision that give those names their meaning.

Bend 2

Bend 2 is the closest relative in workflow. It pairs specifications that people write, in the form of laws, with implementations and proofs that agents write, and it checks the proofs. Lema’s proposal (docs/proposal.md, October 2026) describes how Bend 2 separates a human-authored law, a behavioural def and a proof def, with content-hashed packages and a small proof checker. It also notes that since version 2.0.17, Bend’s ~ templates let a generic theorem be proved once for arguments known at compile time.

Lema takes the division of labour, and the idea that the specifications are what a person reviews. It differs in three ways. It checks with Lean’s kernel instead of a checker of its own. It gives each object (statement, template, proof) its own identity, where Bend hashes packages. And its priorities are general-purpose effects and incremental checking, while Bend’s include fast CPU and GPU execution. The proposal also argues that structures carrying operations and their proofs should be ordinary values that a program can choose at run time. In Bend, closures are affine and ~ arguments must be known at compile time. That is a stated design aim, not a measured comparison.

The older lineage

LCF, the Edinburgh theorem prover of the 1970s, made theorems an abstract type that only the inference rules could construct. However a proof was found, only a small, fixed core had to be trusted. Lema keeps that separation. The elaborator, the tactics and the agents that find proofs are untrusted, and only kernel replay accepts (How acceptance works). Lean differs from LCF in that its kernel re-checks explicit proof terms, but the reason for trusting only the kernel is the same.

Martin-Löf’s type theory made propositions types and proofs programs, with types that can depend on values. Lean’s logic belongs to the line that runs from it through the calculus of constructions. That is what lets a theorem such as twice_id take a proof as an argument and return another.

Smalltalk kept programs in an image, a persistent world of objects edited in place, instead of in source files. Lema also treats the store as the primary artifact and files as views. The difference is mutability. Smalltalk’s objects change in place, while Lema’s objects never change. Names move, and each move is written to the store’s hash-chained history.

Merkle trees fix a whole structure with one hash, because each node’s hash covers its children’s hashes. Lema objects cite other objects by ID, so a declaration’s ID fixes everything it depends on, as a commit’s hash does in Git. The exception is Lean’s Init: its constants are cited by name and pinned by the namespace, not hashed transitively.

The Program core’s sources

The Program core assembles standard constructions:

Later work developed predicate transformers in dependent type theory further, for example Swierstra’s Hoare logic for the state monad (2009) and work on Dijkstra monads in F*, such as “Dijkstra monads for all” (Maillard et al., ICFP 2019). Typestate (Strom and Yemini, 1986) and session types (Honda, 1993) track protocol state in the type system. Lema keeps it in a Contract value instead, for the identity reasons given on the Program core page.

The proposal also names Idris 2 (quantitative types), F* and Project Everest (infrastructure with machine-checked proofs) and Koka (effects) as influences. Lema has no quantitative type system. Single ownership of handles is modelled in contract state and proved through Safe (lean/core/Handles.lean).