11. Formal semantics
Algorithm proves its algorithms in Lean (2150/08). Programming is not mainly about theorems, but a part of it is: type safety, evaluation strategies, scope and binding, subtyping, inference, ownership. For those concepts the site gives the formal view, machine-checked where possible, and labels the strength of the evidence honestly. This document defines the scope, the Lean package, the evidence labels and the link between the formal models and the real languages.
11.1 Evidence labels
Every formal claim on the site carries one of three labels. The label is computed from where the claim's evidence lives (research 01.5: "do not overclaim").
| Label | Meaning | Examples of sources |
|---|---|---|
| proved | a theorem in a proof assistant, checked by our build or by a pinned, cited development | our Prog Lean package; CSLib (Apache-2.0) for STLC safety and normalization and System F<: safety; CompCert and CakeML for compiler correctness facts; RustBelt (Iris, Rocq) for the soundness of the λRust model |
| executable | an executable specification or model that was tested against a real implementation, but not proved | K framework semantics, PLT Redex models (λπ for Python, the Lua 5.2 model), MiniRust, a-mir-formality, WebAssembly SpecTec (the Wasm 3.0 specification is generated by it), JSCert's test262 runs |
| normative | the text of a standard or an official reference | ISO C and C++, ECMA-262, the JLS, the FLS and the Rust Reference (rule ids), the Go spec |
Rules:
- F01: a page may write "proved" only for a claim with a theorem name in
Progor a cited theorem in a pinned external development (by commit and name). - F02: a claim about a model ("STLC is type safe") must not be written as a claim about a language ("Rust is type safe") unless a source proves the link. For Rust, the Aeneas translation has no soundness proof against real Rust semantics in Nov 2026 (01.5); the RustBelt result is about λRust. The page says so.
- F03: a page that cites an executable semantics says which version of the language the model covers and when it was last updated (for example, the K semantics of C was last updated in Feb 2022, 01.5).
11.2 Scope of the Lean package
The package Prog lives in programming/lean/ on the same Lean and Mathlib pin as algorithm (Lean v4.35.0 in Nov 2026; one pin for the whole library, 2150/08.2), and depends on CSLib. Each development is small, readable and linked to a concept node.
| Development | Concept nodes | Contents | Start from |
|---|---|---|---|
Prog.Arith |
evaluation, small-step and big-step semantics | a language of arithmetic and booleans, both semantics, their equivalence, determinism | own (TAPL ch. 3 style) |
Prog.Lambda |
lambda calculus, substitution, capture-avoiding substitution, de Bruijn indices, evaluation strategies | untyped λ, call-by-value, call-by-name, call-by-need (as a heap model), confluence | CSLib (untyped β, η, βη confluence; call-by-name; standard reduction) |
Prog.STLC |
static typing, type safety, progress and preservation, normalization | STLC with base types, safety, strong normalization | CSLib (LambdaCalculus/LocallyNameless/Stlc) |
Prog.Records |
records, tuples, variants, pattern matching, exhaustiveness | STLC with records, sums and variants; a match with an exhaustiveness checker and its soundness | own, on CSLib's locally nameless base (CSLib has no records module in Nov 2026) |
Prog.Refs |
references, mutable state, aliasing, the store | STLC with references; safety with store typing | own |
Prog.Exceptions |
exceptions, error values | STLC with raise and try; the result-type translation and its correctness | own |
Prog.SystemF |
generics, parametric polymorphism, parametricity, type erasure | System F, safety; System F<: from CSLib for bounded quantification | CSLib (Fsub) |
Prog.Subtyping |
subtyping, variance, width and depth subtyping | STLC with records and subtyping, safety, the variance rules for function types | own, with CSLib's F<: |
Prog.Inference |
type inference, Hindley-Milner, let-polymorphism, unification | algorithm W for a small ML, soundness against the declarative system | own |
Prog.FJ |
classes, objects, inheritance, dynamic dispatch | Featherweight Java, safety | own |
Prog.Scope |
lexical and dynamic scope, closures, environments | an environment-based interpreter with lexical scope; the closure conversion; dynamic scope as a contrast | own |
Prog.CPS |
continuations, CPS, tail calls, generators | the CPS translation and its correctness for the call-by-value λ | own |
Prog.Effects |
algebraic effects and handlers, monads in practice | a small language with handlers; safety | own; Default: M4 |
Prog.Ownership |
ownership, moves, borrowing (a toy), affine types | an affine λ-calculus with a borrow rule; safety; a link to RustBelt for the real result | own; the page says it is a toy (F02) |
Prog.Concurrency |
interleaving, data races, linearizability (definitions) | CCS and labelled transition systems from CSLib; bisimulation | CSLib (CCS, LTS) |
The formal field of a concept (04.5) is expected for the concepts in this table and none for the rest, unless an editor sets optional.
11.3 The same lean infrastructure as algorithm
The Lean side reuses algorithm's tools without change:
prog lean build(the same code asalgo lean build): lake build, the axiom check (nosorry, only the standard axioms), the theorem name links from pages to Lean declarations.- The
formalizerandproveragents (14.2) with the same prompts and ladders, and the same review rules. - Lean code is Apache-2.0 (19.2), as in algorithm.
11.4 Notation on the pages
Formal sections use the usual notation of the field (inference rules, judgments Γ ⊢ e : τ, reduction e → e'), rendered with KaTeX, and an inference-rule block:
:::rule T-App
Γ ⊢ e₁ : τ₁ → τ₂ ;; Γ ⊢ e₂ : τ₁
---
Γ ⊢ e₁ e₂ : τ₂
:::
Each rule on the page links to its Lean constructor. A theorem on the page links to its Lean theorem. The formal section of a concept page (6.3, "Theory") is short and comes after the practical sections, because most readers do not need it.
11.5 Grammars
Syntax is formal too. For each tier-1 language, the site keeps the grammar of the language in a machine form when the language publishes one (Python's PEG grammar, the Go spec's EBNF, the ECMAScript grammar, the JLS grammar, the C and C++ grammar summaries by clause, the Rust Reference grammar), with the source and the licence. Feature pages show the productions they are about (6.3, Synopsis), rendered as railroad diagrams (12.5). Where the grammar's licence does not allow copying (ISO standards), the page cites the clause and shows our own simplified form, marked as simplified.
11.6 Differential tests against real languages (F3)
The F3 level (04.9) needs the formal model to agree with real languages on generated programs:
- Each Lean development that defines an interpreter (
Prog.Arith,Prog.Lambda,Prog.STLC,Prog.Records,Prog.Refs,Prog.Exceptions,Prog.Scope) has a translator from its syntax to two or more real languages (for example to Python, OCaml and JavaScript for the call-by-value λ; to OCaml, Haskell, Rust and TypeScript for STLC with records). - A generator makes random well-typed programs (from the Lean side, with
Plausible). - The harness runs each program in the Lean interpreter (compiled with
lake exe) and in each real language (in the images of 07.4), and compares the results. A difference is either a bug in the translator, or a real difference between the model and the language, which becomes a documented "where the model and the language differ" item on the concept page (for example: integer overflow, evaluation order of arguments in C, the late binding of closures in Python loops). - This is how the site connects "proved" to "executed" without overclaiming: the proof is about the model, the test is about the language, and the page shows both labels.
11.7 What is out of scope
- Proofs about real compilers or real language specifications. We cite CompCert, CakeML, RustBelt and similar work; we do not reproduce them.
- The mathematical theory of semantics (domain theory, categorical semantics). It belongs on math2; a programming page links it.
- Verification tools as a subject (Dafny, Frama-C, SPARK, Verus) are in scope as
toolnodes with executed examples (their verifiers run in the images), in theprogram-analysis-and-verificationarea. Those examples are labelled proved only for what the verifier checked, with the verifier's version.