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

Realization

A model that type-checks is not yet a running system. Two things stand between the source and a database that answers questions: the executor must know it can evaluate the program at all, with a cost it can name, and the program must become an artifact a runtime loads and replays. Argon settles the first before the second. A program declares how hard it is to reason about, the classifier verifies that claim, and only a program the executor can run reaches the artifact.