Running it
Learnable in an evening. Judged at every step.
Five verbs, one command, and a guided tour that hands you the way to break every promise it makes. No board is needed for any of it — it runs on a plain laptop.
The whole loop is the same five verbs the machine lives by, judged and planned by one binary, harb, and booted by one script. There is no configuration to discover and no hidden state to unravel. Every command tells you what it did and why.
Write a .machine file. Every line must say why it is there.
harb checkThat is, check it against the language's rules before anything runs: every line one the language knows, every program granted what it asks for, every part saying why. It accepts the file, or refuses it with the line and the reason in plain words: alerts needs network, which no declaration grants.
harb planSee the order things will happen in, before any of it does. A mistake is caught here, not at 2 a.m.
One script builds the image and boots the whole machine in QEMU, a program that imitates a computer. The machine prints a line for every step, and at the end compares what it printed, line by line, with what the file says a correct boot prints: bash experiment/os2_image.sh qemu_egress. The README's Try it lists what the first boot needs installed.
Change one line and watch the machine catch the difference. A guarantee you have only seen succeed is a claim.
No board is needed to learn any of this — it runs on a plain laptop.
$ harb learn a guided tour of a declared machine, in 18 lessons. I. THE DECLARATION 1 · 2 · 3 II. THE BOOT 4 · 5 · 6 III. WHAT A WORLD MAY DO 7 · 8 · 9 · 10 · 11 IV. WHO A DEVICE IS 12 · 13 · 14 V. THE NETWORK 15 · 16 VI. THE FLAGSHIP 17 · 18 harb learn <n> one lesson, in full harb learn <n> --run and run its command harb learn --words a world, a pin, a court
six worlds · one command · only NEEDS differ world declared eth0 /data fork sealed process, filesystem absent mounted permitted still network, filesystem present mounted REFUSED open process, network, filesystem present mounted permitted blind process absent empty permitted ledger all three, SEES [data] present mounted permitted caisse all three, SEES [logs] present empty permitted ── none of this grid is declared — it is worked out FROM what each world asked for. what a world did not ask for, the kernel does not give.
judged by name, twice — two texts keep them, neither keeps all, so the box is not flattered against the board's EXPECTATION: always reachable KEPT a stable name KEPT a durable log KEPT survives the cut NOT KEPT 4 promised, 3 kept against what the emulator PRINTED: always reachable NOT KEPT no wire in QEMU a stable name NOT KEPT a durable log KEPT survives the cut NOT KEPT watchdog off 4 promised, 1 kept — the honest number, until a card goes into a real Pi 4
A guarantee you have only ever seen succeed is a claim; one you have watched refuse you is evidence. So the tour hands you the way to break every promise it makes.