pflow-polyglot is a repository with one idea in it: a single coffee-machine Petri net, implemented over and over, with every implementation held to a byte-identical six-line trace. The interesting axis is not the languages — it is the forms: the same net encoded as runtime data (interpreter), as pure functions (lambda), as generated code, and as a public API surface (contract). Four encodings, one golden trace, and a Bazel gate that fails if any of them drifts.
This week the repo picked up a tenth language and, because of it, a fifth form. The language is Lean 4. The form is called proof, and the reason it exists is the point of this post: the theorem declaration in the Lean version is line-for-line equivalent to a runtime check the other languages were already capable of. Writing them side by side is the clearest illustration I have found of what a proof assistant actually buys you — and what it doesn't.
Lean went in the ordinary way first: interpreter, lambda, and contract forms,
mirroring the Haskell ones. Pure functions, Option Marking doing the work the
imperative languages need a prepare/execute split for. Nothing exotic.
But the language kept editorializing. The interpreter form's scheduler — "fire
the first enabled transition until none is enabled" — had to be declared
partial def, because termination of that loop is a property of this net,
not something the compiler can see from the code. Every other language in the
repo runs the same loop without comment. Lean is the only one that makes you
put in writing that you haven't proven it stops.
That asymmetry nagged. The repo's whole premise is that every implementation
makes the same claims about the same model. Lean was pointing out, correctly,
that most of those claims were assertions — comments, at best. The net is
1-safe: says who? Every form carries an enablement clause that refuses to fire
a transition into a marked place, and the README asserts the clause matches
capacity: 1 in the model. Nobody checks that the clause ever matters.
The fifth form drops the assertion and does the work. Two changes to the setup:
Then, before printing anything, the program explores the entire reachable state space by breadth-first search and verifies two claims:
Claim 1 — 1-safety is structural. No reachable marking holds two tokens
in any place, even without the capacity clause. This is the claim that
licenses every other form's set representation: the clause they all enforce is
never load-bearing, and a Set loses nothing a multiset would keep.
Claim 2 — the outcome is confluent. The net has no conflict — no two
transitions compete for a token — so every maximal firing sequence ends in the
same deadlock, and it is exactly {Payment}. The golden trace's final line is
not one schedule's artifact; it is the only place the net can stop.
The search needs no bound to terminate: a marking that violates claim 1 fails
immediately, so the explored space is a subset of {0,1}^10 — at most 1024
markings. This net reaches 16.
Only after both checks pass does the interpreter's scheduler run and print the canonical trace. A violation exits nonzero before the first line, which fails the parity gate mechanically: a program that dies cannot print six lines.
Here is the shape of claim 1 in Python — a startup model-check, run on every execution:
def verify():
seen = {INITIAL}
frontier = deque([INITIAL])
while frontier:
marking = frontier.popleft()
if any(count > 1 for count in marking):
return f"1-safety violated: reachable marking {marking}"
...
Go, Rust, JavaScript, and — with some ceremony around associative arrays — Bash all say the same thing. And here is the Lean:
def reachable : List Marking :=
explore 1024 [initialMarking] [initialMarking]
def oneSafe (m : Marking) : Bool :=
m.all (· ≤ 1)
theorem reachable_one_safe : reachable.all oneSafe = true := by decide
theorem unique_deadlock :
(reachable.filter isDeadlock) = [finalMarking] := by decide
explore is the same BFS the other five languages run — same frontier, same
seen-list, same successor function. decide tells the kernel to evaluate
it: the proposition is decidable, so run the decision procedure and check it
returns true. This is proof by reflection, and the honest way to say it is
that the theorem is the Python function. Same algorithm, same 16 markings,
same comparison at the end. Nothing about the Lean version is smarter.
What differs is when it runs and what failure means:
| check runs | failure means | |
|---|---|---|
| Go, Rust, Python, JS, Bash | at startup, every run | exit 1, no trace |
| Lean | once, during elaboration | the program does not compile |
In Lean, main cannot exist unless the net is safe. There is no code path in
the shipped artifact where the check failed, because the artifact is only
produced after the kernel has watched the entire state space get explored.
The runtime versions re-establish the same fact a few microseconds before
every run; the Lean version established it once, and the binary is the
receipt.
A check you have never seen fail is an assertion with better marketing, so:
mutate the net. Make PourCoffee produce a token into Payment — the place
it reads as a guard — and the net can mint payments. Two tokens in one place,
1-safety gone.
Python, at startup:
proof failed: 1-safety violated: reachable marking (0, 0, 0, 0, 0, 0, 0, 0, 2, 0)
exit 1
Lean, at compile time:
error: Tactic `decide` proved that the proposition
reachable.all oneSafe = true
is false
Same defect, same detection, same BFS finding the same marking. One reports it
as a process exit; the other reports it as the nonexistence of the program.
I find the second error message genuinely delightful: it is not "assertion
failed," it is "I proved your claim is false" — the kernel ran the search,
found the counterexample, and refused to let main be defined on the other
side of it.
The pitch for proof assistants usually leads with what is unreachable for ordinary languages: dependent types, mathlib, verified compilers. All real. But the on-ramp is much shorter than that, and this repo now demonstrates it in the most literal way I could construct:
explore in Lean is
verify() in Python with the mutation swapped for recursion.The entire delta between "runtime model-check" and "machine-checked theorem"
here is the word theorem and the tactic by decide. That's it. The proof
form in Go and the proof form in Lean are the same program; Lean just runs the
interesting half of it inside the compiler and makes the result a
precondition of the program existing.
There is a real boundary, and it's worth naming: decide works because the
state space is finite and tiny. The moment the claim quantifies over an
infinite domain — every net of a given shape, every initial marking, every
fuel value — evaluation stops being a proof strategy and you need induction,
invariants, actual mathematics. The three theorems in
lean/proof.lean
sit deliberately on the near side of that boundary, where a theorem is just
another port of a program you already had. The far side is where it stops
being a polyglot exercise — one net, proven safe for all markings, is a
different post.
The repo now stands at 39 programs: five forms across ten languages, gaps deliberate (Solidity cannot model-check itself at startup; Ruby, Julia and Haskell proof forms are open invitations). Twenty programs run under the hermetic Bazel gate, the rest under the native-toolchain gate, and every one of them — interpreter, lambda, generated, contract, proof — prints the same six lines:
Step #1: BoilWater => BoiledWater,CoffeeBeans,Cup,Filter,Pending
Step #2: GrindBeans => BoiledWater,Cup,Filter,GroundCoffee,Pending
Step #3: BrewCoffee => CoffeeInPot,Cup,Pending
Step #4: Send => CoffeeInPot,Cup,Sent
Step #5: Credit => CoffeeInPot,Cup,Payment
Step #6: PourCoffee => Payment
Thirty-three of them assert that trace is right. Five more re-derive the justification at every startup. One of them proves you couldn't have gotten a different one — and won't compile for a net where you could.