2. A Note on This Document🔗

A complete API reference, every definition and theorem with its docstring, is generated by doc-gen4 and hosted alongside this book at the API reference.

This book is generated by Verso, the documentation system of the Lean language. Every Lean code block is elaborated by the same compiler that checks the whole development, so nothing in this book can drift silently out of date. For example, the following is checked as you read it:

Diagrams are generated by Lean as well. The central result of the preceding section, that the optimised interpreter and the published specification reduce a term to the same answers, is the commuting square below, drawn here as a preview and proved in the correspondence chapter:

The remaining chapters cover the object language, the minimal interpreter and its standard library, the gradual type system, the metatheory, the operational semantics and its correspondence to the interpreter, the blockchain-oriented guarantees, the future-work branch, and a discussion of the development's current limitations and open problems.