W0

W0: warp's types, proved

W0 is a small model of warp's type system, written in Lean 4, with a machine-checked proof that a program it accepts never gets stuck: it ends in a value of its type, raises an error, or runs forever. Warp's many checks are tied to that one model by tests, so they cannot drift apart.

warp types shows how a program reads in W0 and what both sides say:

warp types app.warp

x = 3
x = "a"

W0: [.bind "x" .var none (.int (3)) false, .statement (.assign "x" (.text "a"))]
model: Rejected
warp: Rejected: "x was an Int, is given a Text: use another name at 2:5"

The rule is: whatever W0 rejects, warp refuses at compile time. Warp may refuse more (an ambiguous line, say), never less. A program warp compiles but W0 rejects is a hole; each known hole has a card and a test that fails once it is fixed. Today two remain: b: bool = no; b++ and a function assigning a text to its number parameter, f(n) := { n = "x"; n }; f(3).

The model covers numbers (bool ≤ int ≤ exact ≤ number), texts, lists, maps, optional types and ??, classes and sum types, functions, lambdas, and stored errors. The first warp types builds the model, says so and waits up to 15 minutes for it; after that a run takes about a second.

The laws of a program are proved with the same prover: laws.