1.1. How this guide is organised🔗

The three Laurel guides are aimed at different readers, and this one is for the person writing Laurel — typically inside a front-end compiler:

• this User Guide describes what you can write and what it means;

• the Designer Guide records why the language is shaped the way it is, and what is planned;

• the Implementor Guide describes the compilation pipeline and how Laurel lowers to Core.

Within this guide, Syntax is the grammar: lexical rules, precedence, and the surface productions. Execution covers the features whose meaning does not depend on verification — the ones a reader with an ordinary programming background will recognise, and the ones that behave identically when a program is concretely interpreted. The Verification sections cover features whose whole purpose is analysis: they may be erased or approximated when the program runs, and they are introduced in order of increasing difficulty — first the ones that do not involve the heap (Fundamentals), then the heap-specific ones (Objects), then contracts on the exits and suspensions that exceptions and coroutines introduce (Continued), then proof debugging.

A feature that has both an execution and a verification side appears in both places rather than in a section of its own. Exceptions and coroutines are the two: throw / try / catch and coroutine / yield / resume are described where the other execution features are, while throwsOn and relies / guarantees are described with the other contracts.