Everything deserves a theory

“Theory” is a big word. It sounds like physics, or a chapter of a mathematics book: something distant and abstract, written by experts for the ages. Not something you would have for your elevator, or for the way your company approves an invoice.

We think you can have one, and that you should.

What a theory looks like

For an elevator: the floors, the doors, the cabin and the buttons; how a press or a sensor moves it from one state to the next; and the requirements. The doors are never open while the cabin moves. Every call is served, sooner or later.

For an invoice process: the documents, the people, the steps and who may take each one; and the rules. Nothing is paid without two approvals. Nobody approves their own expense.

The same goes for anything, however small, that has rules to follow or requirements to meet. A hotel never sells a room twice for the same night. Two discounts never stack beyond what the policy allows. A visitor’s badge never opens the server room. The boiler never runs when no room needs heat.

None of this is abstract. It is what an engineer or a process owner already knows, partly in their head and partly in documents. The difference is that a theory states it in a language a machine can check, Lean in our case, so its meaning is exact.

The systems companies run on

Software is no different. We think every piece of software is critical to someone. Critical used to mean aircraft and power plants. Today it also means the rule that stops an intrusion and the program that schedules a hospital’s operating rooms. They deserve the same care.

Three kinds of system matter most to us.

Programs. A program has a meaning nobody fully keeps in mind. A theory writes it down, so that a change, or a rewrite in a new language, can be checked against the original for every input, not only for the cases someone remembered to test.

Rules and policies. The rules that watch a running system for intrusions, the policies that decide who may do what: each is a small formula, and a set of them grows for years. Which rule can never fire, which two say the same thing, what an exception quietly took away: a theory can answer, with an event that shows it or a proof that none exists.

Processes. Approvals, separation of duties, the steps an order goes through. They live in manuals and in software configurations at once, and the two drift apart. A theory of each lets you check that the software still does what the manual says.

What it gives that tests don’t

Without a theory we learn about a system by trying it. A test runs one case and tells you what happened in that case. A thousand tests tell you about a thousand cases. That is good engineering, and we keep doing it.

But tests leave open the questions that matter. What happens if someone calls from another floor just as the cabin leaves? If two buttons are pressed at the same instant? If the doors are blocked while a call arrives? Each is a case a test may or may not try, and there are always more. What we want to know is whether, in any of them, the doors can open while the cabin moves, or a call can be forgotten. That question is about every possible input, in any possible case, including the ones nobody thought to try. No number of tests answers it.

A theory does. Once the elevator has one, “the doors are never open while the cabin moves” becomes a theorem: proved for every sequence of calls, in every state. Or it is refuted, by one concrete sequence that breaks it. Either answer is worth having. The proof closes the question. The counterexample is the bug, found before anyone rode it. Sometimes neither comes easily. Then the theory says exactly what is still open, instead of guessing.

A theory is about a model of the system. What the model leaves out, the motor, the wiring, still needs testing.

Why now

For decades formal methods were reserved for a few large, critical undertakings: avionics, railway signaling, chips. Building a theory took specialists years, and checking it took tools few people could use.

Three things changed. Proof assistants such as Lean became usable programming languages, with large shared libraries and a small kernel that checks every step. They became fast enough to work on real systems. And AI can now help write the theory. Together they put a theory of an ordinary system, an elevator controller, a set of business rules, a rule language, within reach of a small team. Formal methods are no longer only for the largest projects.

Within reach is not the same as automatic. A good theory takes insight: deciding what to model and what to leave out, and stating the requirements so they say what you mean, no more and no less. AI can help with the writing; the insight is the craft.

And AI

AI now writes code, rules and configurations faster than anyone can read them. Much of it is right. Some of it is plausible and wrong, and reading does not tell the two apart.

Checking against a theory can. The AI proposes; the theory decides whether the proposal meets the stated requirements, for every input, and when it does not, it shows the case. What the theory cannot decide is whether the requirements are the right ones. That stays with people, and it is where their judgment belongs.

So yes: your elevator deserves a theory, and so does your process, and your longest-lived program. What comes out is proved, not just plausible.