Cairn docs

Cairn apps are written in Lean 4. The app's state, its view, its layout, its hit testing and its text editing are pure Lean functions, and every thing a person can do is a claim: an id like ^2, a sentence saying what happens, a formal statement, and a proof that the code meets it. A thin Swift host runs the app on macOS and paints it with Metal.

These docs are young. Pages that today's code supports are written; the one that isn't says what it will cover and what has to land first. Every code sample is included from a source file that make check compiles, so a sample can't drift from the code it shows.

Guides

Building an appFrom a first window to effects and shipping, one chapter at a time. Apps on CairnThe example apps: packages of their own, each with its claims. Try an appCounter, Basics and TodoMVC in the browser, every control with its claim id and evidence.

Reference

API referenceEvery module, declaration and claim in Cairn, generated from the code by cairn doc. The cairn toolStarting, building, checking, bundling, documenting and publishing a package. ClaimsEvery claim kind, what each generates, and what the build checks. The evidence ladderProved, fuzzed, tested, seen, assumed: how sure we are of each claim. How much to trust a claimWhat each kind of evidence rules out, what it still trusts, and a bug the tests miss. The trusted baseWhat the proofs rely on but can't prove, and how each piece is checked. Release notesWhat changed in each version, and what an app can rely on across them.

Evidence

Claim pagesEvery claim each package makes, grouped by place, with its proofs, generated from what it published.

Contributing

The host protocolThe two byte buffers between Lean and Swift, and the threads around them. Writing host effectsAdding something the host does for an app, with its assumption and fuzz check. Profiling against a referenceMeasuring an app against the one it replaces, with Apple's own tools. ContributingThe rules every change follows.