Tutorial¶

Welcome! Algae is a small proof and algebraic-specification language. You hand it a vocabulary (sorts and operators), a few facts (axioms and inference rules), and then you prove things — by building explicit proof trees that a tiny, deeply suspicious kernel re-checks step by step. No hand-waving survives.

This tutorial runs entirely in your browser. Every alg block below is a live editor backed by the real kernel compiled to WebAssembly — edit it, press Check ▶, and watch the kernel object. We start from the ground up: the editor, then just enough logic, then how Algae writes rules and assembles proofs, and finally sorts, specifications, and equational reasoning. The later chapters work through the real standard library — core, nat, list, group, monad — so nothing here is throwaway toy code. It all imports, and it all verifies.

Tip

You don’t have to memorise a wall of syntax before your first proof. Break things on purpose; the kernel is unbribable and will point at exactly where you went wrong. And when you’re not sure what to write next, leave a hole — the editor will tell you the goal and even suggest the fix.