Examples

The three worked examples from the specification (§18), each as its source with the ledger the compiler wrote beneath it. They are the integration tests, and every mechanism in the language appears in at least one.

Each page shows the program’s files, then what onus review reported for it: every obligation in the entry module with its state, and the path report for any path the program declares. The numbers are read at build time from the review output committed under examples/ in the repository, so they are the compiler’s own, as of the last run that was committed.

Example: Mandelbrot

The first worked example (spec §18.1). Pure computation with refinements, a loop with an invariant and a measure, an example block, a property, and a root capability for the one file it writes.

24 proved · 1 checked · 0 assumed

Example: monthly report

The second worked example (spec §18.2). A read-only SQL report, a query checked at compile time by the SQL library’s own parser, and a path that forbids writing.

5 proved · 0 checked · 0 assumed · 1 path

Example: checkout

The third worked example (spec §18.3). A payment endpoint across four modules, with a sealed type as evidence of authentication, an asserted claim, a policy on assumptions, and the path report the home page renders.

9 proved · 0 checked · 0 assumed · 1 path

Further on