Concepts

These pages explain why L4 works the way it does: the choices behind its syntax, how it models legal rules, and what its type system guarantees. Read them after you have tried a feature. For what a keyword does, see the Reference; for step-by-step guides, see the Tutorials.

Language design

• Design principles: the five principles behind L4, and the style of writing that follows from them.
• Reading like the law: how L4 borrows from English grammar so that code can be checked against its source text.

Legal modeling

• Definitions and duties: why L4 keeps rules that define things apart from rules that impose duties.
• Exceptions and defaults: how to encode a general rule followed by its exceptions.
• How obligations unfold: a contract as something that waits for events and moves through time.

Types

• Types as legal categories: records and enumerations as the shapes of legal definitions.
• Exhaustiveness: why L4 checks that a determination handles every case.
• Type theory: the formal foundations, for readers who know type theory.