Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Explanation

Explanation pages cover why the system is the way it is. They are essays, not recipes. Each one is built in two tiers:

  • An In plain terms opener (3-5 sentences) that names the concept and gives the working-developer analogue. You can read the entire quadrant at this level and come away with a working mental model.
  • A formal section that names the underlying construction and points into the reference and semantics pages where it is precisely defined.

The pages here, in increasing order of formality:

PageTier
What panproto solvesPlain
Schemas as theoriesPlain, with one formal section
Migrations as morphismsPlain, with one formal section
Lenses and round-trip lawsPlain, with the three laws stated formally
Layout enrichmentPlain, with the section law stated formally
Composing protocols by colimitPlain, with one formal section
Schema version control semanticsPlain, with one formal section
What panproto verifiesCatalogue of mechanically-checked properties
ArchitectureCrate dependency graph and the layering that holds the system together

The denotational semantics cluster is separate and load-bearing. It is the place where the implementation is pinned to a precise mathematical specification: the expression language, the lens DSL, the theory DSL, the pushout-based merge, and protolens composition. Each of those pages still opens with a plain-terms section, but the body is dense.