Playground

A full-page editor for experimenting with Algae. It is seeded with the standard library’s nat module — a complete, checked development of the natural numbers, including a proof by induction. Edit anything and press Check ▶ to re-run the kernel.

Everything runs locally

The proof checker is algae-kernel compiled to WebAssembly. Your code never leaves the page. The other standard library modules (core, list, option, result, group, monad, adt) are available via import.

Load

Load and share proofs by URL

Paste any URL into the box above and press Load to open that .alg file in the editor — a game room like game/challenge/060-room.alg, or an absolute link such as a raw GitHub file (https://raw.githubusercontent.com/dhilst/algae/refs/heads/main/algae/v1/challenge/002-room.alg).

The address updates to playground.html?q=<url>, so that link is itself shareable — send it to anyone and the playground loads the proof automatically. (Cross-origin hosts must allow it via CORS; raw GitHub does.)

If a proof is incomplete

A proof that ends in wip, or that leaves a hole _ where a real step is required, checks as in progress rather than done — the results pane tells you so. Fill in the holes and check again.

Suggested fixes

When a check flags a fixable error — a wip/qed terminator that doesn’t match the proof, a by wip(?goal) hole with candidate tactics, or a tactic hole that suggests a continuation — you can apply the fix without retyping it. Click the flagged text (or press Ctrl-Space) to see the suggestions, then pick one to rewrite the source; the checker re-runs automatically so the next suggestion is ready. Hole candidates seed a complete by <tactic>?; step, so the next check guides you to its arguments.