# Cairn

> Research into user interfaces where every action a person can take is a claim with a durable id and machine-checked evidence.

Apps are written in Lean 4: the state, the moves a person can make, the view and the layout are pure functions, and each move, flow and invariant is a claim with an id (`cairn^N`, written `^N`) that is never reused. Proofs live next to the code and are checked by Lean's kernel with only the standard axioms. What can't be proved is fuzzed, tested on the running app, captured on screen, or recorded as an assumption. A thin Swift host runs the app on macOS with AppKit and Metal and makes no decisions of its own. Cairn is research: it runs on macOS 27, and its APIs change between releases.

Every docs page below is Markdown, with its code samples included from the source that `make check` builds. The API reference is generated from the code and lists every claim with its evidence.

- [Cairn docs](https://cairn.iamnbutler.workers.dev/docs/index.md): How to build a Mac app in Cairn, where everything a person can do is a claim with a durable id and machine-checked evidence.
- [All the docs in one file](https://cairn.iamnbutler.workers.dev/llms-full.txt)
- [API reference](https://cairn.iamnbutler.workers.dev/docs/api/llms.txt): every module, declaration and claim of the framework, with each claim's evidence

## Guides

- [Building an app](https://cairn.iamnbutler.workers.dev/docs/guide.md): Building an app in Cairn, one chapter at a time, for someone who has never seen it.
- [Your first app](https://cairn.iamnbutler.workers.dev/docs/guide/first-app.md): What a Cairn app is made of, how to run one, and how to start your own.
- [Moves and flows](https://cairn.iamnbutler.workers.dev/docs/guide/moves-and-flows.md): Declaring what a person can do, the paths through it, and what must always hold.
- [The view and layout](https://cairn.iamnbutler.workers.dev/docs/guide/view-and-layout.md): What an app shows, as a tree of boxes and text that Lean lays out in whole points.
- [Proving a claim](https://cairn.iamnbutler.workers.dev/docs/guide/proving.md): The proofs an app needs, from a move's one-liner to "the control is on screen exactly when its move is enabled".
- [Effects and the host](https://cairn.iamnbutler.workers.dev/docs/guide/effects.md): Time, timers, files, sounds and the network, without a line of IO in the app.
- [Shipping](https://cairn.iamnbutler.workers.dev/docs/guide/shipping.md): Checking an app, putting it in a signed bundle, and publishing it with its claim pages.
- [Apps on Cairn](https://cairn.iamnbutler.workers.dev/docs/examples.md): The example apps, Pairs, Sky and Yap, each a package of its own with its claims on the registry.
- [Yap](https://cairn.iamnbutler.workers.dev/docs/examples/yap.md): Porting a real dictation app to Cairn one to one, with its original as the spec.

## Reference

- [API reference](https://cairn.iamnbutler.workers.dev/docs/reference/api.md): Every module, type and declaration in Cairn, and every claim it makes, generated from the code.
- [The cairn tool](https://cairn.iamnbutler.workers.dev/docs/reference/cairn-tool.md): The command line for Cairn packages. It starts a package, adds dependencies, builds, checks, bundles, documents and publishes it.
- [Claims](https://cairn.iamnbutler.workers.dev/docs/reference/claims.md): Every claim kind, its clauses, what it generates, and what the build checks.
- [The evidence ladder](https://cairn.iamnbutler.workers.dev/docs/reference/evidence.md): How sure we are of each claim: proved, fuzzed, tested, seen or assumed, computed by the build and shown on the claim pages.
- [How much to trust a claim](https://cairn.iamnbutler.workers.dev/docs/reference/trust.md): What each kind of evidence rules out, what it still takes on trust, and a bug that tests miss and a proof can't.
- [The trusted base](https://cairn.iamnbutler.workers.dev/docs/internals/trusted-base.md): Everything the proofs rely on but don't prove, and how each piece is checked instead.
- [Release notes and compatibility](https://cairn.iamnbutler.workers.dev/docs/reference/releases.md): What changed in each version of Cairn, and what an app can rely on across versions.

## Evidence

- [Claims](https://cairn.iamnbutler.workers.dev/docs/evidence.md): Everything a person can do in a Cairn app is a claim, with an id that never changes, a promise, and a proof that the promise holds in every state.

## Contributing

- [The host protocol](https://cairn.iamnbutler.workers.dev/docs/internals/host-protocol.md): Two byte buffers, three functions and three threads: everything that crosses between Lean and the Swift host.
- [Writing host effects](https://cairn.iamnbutler.workers.dev/docs/internals/host-effects.md): How a new kind of request reaches the host, and what it takes to trust the answer.
- [Profiling against a reference](https://cairn.iamnbutler.workers.dev/docs/internals/profiling.md): How Cairn measured its port of Yap against the original, with Apple's own tools so the harness can't flatter the result.
- [Contributing](https://cairn.iamnbutler.workers.dev/docs/internals/contributing.md): The rules every change to Cairn follows, and the one command that checks them.

## Optional

- [Blog](https://cairn.iamnbutler.workers.dev/blog/): a post for each milestone, what it set out to show and what it can't yet, with videos
- [Packages](https://cairn.iamnbutler.workers.dev/packages/): the package registry, with each version's claim ledger
- [Source](https://github.com/iamnbutler/cairn): the repository