Most WooCommerce bugs I get called in for have the same shape: some code trusted data it should not have. The bug is a negative line total, an order status nobody defined, or a coupon stacked on top of itself. PHP runs all of it without complaint, which is why the Lean proof assistant caught my attention this week.
Ronen Lahat wrote an introduction to Lean for programmers on Towards Data Science, aimed at developers who already know other languages and find the syntax strange. Lean is a proof assistant and a functional language: its checker verifies every step of a mathematical proof before anything runs. You will not ship a Lean plugin to a client, but the habits behind it still transfer.
What does the Lean proof assistant do?
It rests on the Curry-Howard correspondence: propositions are types, proofs are programs. Implication is a function signature, conjunction is a tuple, and proving a theorem means writing a term that satisfies the type. Lahat’s example, (P → Q → R) → (P ∧ Q → R), has a proof that is nearly identical to the statement itself. A small kernel checks the result, and the term either inhabits the type or it doesn’t. The author’s confidence doesn’t count for anything.
Why can’t PHP prove anything about my store?
PHP types only describe the shape of a value. Lean has dependent types, where a type can depend on a value, for example a type that says a natural number is at least zero. PHP and TypeScript have nothing like it, so on the web we approximate with runtime validation, which is what Zod does. That’s the same idea as why validation beats guessing in WordPress. The rule I take from it is to check where data enters, once, and then pass around values that already passed. When the checks are scattered across templates, the same bad value tends to get validated in three places and still slip through.
What can I copy into PHP tomorrow?
The nearest thing to a proof being a term is a value object whose constructor refuses bad input. If the constructor is the only way in, holding the object means the check ran.
<?php
final class bbioon_PositiveAmount
{
public readonly float $value;
public function __construct(float $value)
{
if ($value <= 0) {
throw new InvalidArgumentException(
"Amount must be positive, got {$value}"
);
}
$this->value = $value;
}
}The only way to hold one is to have passed the check, which is a weak version of what Lean gives you for free. I use the pattern for money, order statuses, and coupon scopes. On functions.php-heavy projects it belongs in a small layer of your own rather than scattered helpers.
If you inherited a store where every function re-checks the same array, that’s work I take on: find the entry points, wrap the money and status values, and leave tests behind.
What is sorry, and why should I steal that habit?
Lean lets a proof compile with sorry in it and prints “declaration uses ‘sorry'” as a warning. That is the honest version of TypeScript’s any: the gap stays visible. Our equivalents are @phpstan-ignore, TODO comments, and casts to (float) where nobody knows the type. Keep them loud and greppable. Across many client sites, grep is how you find the gaps before a client does.
Is Lean worth a WordPress developer’s time?
Not for the deliverables, and I wouldn’t pitch it to a store owner. Mathlib, its community library, holds 1.6 million lines of formalized math, and Terence Tao now does AI-assisted Lean proofs on stream. None of that touches a checkout page. An hour with it does change how you read a type error, and it’s a decent way back into math you skipped. I’m not sure the tactics part transfers without doing the math. The official learn page lists Functional Programming in Lean as the entry point for programmers.
Concrete next step: open the live Lean playground, type example : 2 + 2 = 4 := rfl, then delete the rfl and read the error. You can feel that loop between goal and proof state in five minutes.
