Can You Prove a Computer Program Will Never Crash?
A Bug in Your Code: Testing Isn’t Enough
You write a small program for a school project: a simple adventure game. It runs fine most of the time, but once in a while the screen freezes when your character tries to open a locked door. You test it by clicking everywhere you can think of, and eventually you can’t make it crash anymore. Is it truly bug-free? Probably not — you just haven’t hit the right weird sequence of clicks yet. That’s the heart of a deep problem: testing can only sample a few possible paths through your code, but a program can have billions of possible paths. To be really, truly sure a program won’t misbehave, you need a proof — the same kind of airtight reasoning you’d use in geometry.
In the late 1960s, computer scientists started asking: can we treat programs like mathematical objects and prove things about them? That led to a family of ideas called dynamic logic, a system for talking about what programs do, step by step, using the tools of modal logic. This logic doesn’t just test a program; it reasons about every possible execution, all at once.
Talking About Programs with Logic
To see how dynamic logic works, picture your computer’s memory at one instant as a state — a snapshot of everything the program knows: the value of a variable, the player’s position, which door is open. When a program runs, it moves from one state to the next. So a program can be thought of as a relation between pairs of states: if starting in state x, the program can finish in state y, then x and y are connected by that program.
Dynamic logic gives us two ways to look at a program. First, we can say that a statement about a state is true or false there. For example, “the player’s score is over 100” might be true in state x. Second, we can embed programs inside our logical sentences. The expression [α]A means “in every state you can reach by executing program α, the statement A holds.” This is similar to the idea of necessity in modal logic, where a box □ means “in all possible worlds.” And the expression ⟨α⟩ A means “there is some execution of α that leads to a state where A is true” — like the possibility diamond ◇.
So with just a few symbols, we can make precise claims about programs. For instance, if α is your “open door” routine, [α] (door_is_open) says that after running that routine, the door is always open, no matter what.
From Hoare Triples to Modal Boxes
The starting point for dynamic logic was a 1969 paper by the British computer scientist C.A.R. Hoare (born 1934). He introduced a notation we now call a Hoare triple: {A} α {B}. It means: if statement A is true before you run program α, then B will be true after it finishes — assuming it does finish. (A is called the precondition, B the postcondition.) For example, {x=3} x := x+1 {x=4} is obviously correct. But for loops, the reasoning gets tricky.
Hoare’s system included rules for proving such triples. One rule said: if program α1 turns a state satisfying A into one satisfying B, and α2 turns B into C, then running them in sequence — α1;α2 — turns A into C. Another rule handled while loops: if running the loop body α while a condition B is true preserves the truth of A, then when the loop finally exits, we can conclude both that B is false and that A still holds.
In the mid-1970s, the American computer scientist Vaughan Pratt (born 1944) realized that these Hoare triples could be translated into modal logic. The triple {A} α {B} becomes the PDL formula A → [α]B: “if A is true, then every terminating run of α ends with B true.” Suddenly, all of Hoare’s rules could be tidily derived from just a few axioms of a new logic — Propositional Dynamic Logic (PDL) — introduced by Michael J. Fischer (born 1942) and Richard E. Ladner (born 1943) in 1979. PDL stripped away the first-order variables and concentrated on the pure logic of program connectives: sequencing (;), non-deterministic choice (∪), iteration (*), and test (?).
The Rules of the Game: Axioms for Reasoning
PDL works on labeled transition systems (LTS) — graphs whose nodes are states and whose edges are labeled with the names of atomic programs. An edge from state x to state y labeled π means: there is a possible execution of π that leads from x to y. A valuation says which simple propositions (like “the door is open”) are true at each state.
Complex programs are built up just like complex sentences. α;β means “first do α, then β.” The relation for α;β is the composition of the two binary relations: you can get from x to y by α;β if there’s some middle state z with x connected to z by α and z to y by β. α ∪ β is non-deterministic choice: you can go where either α or β could take you. α* means “repeat α zero or more times” — think of a loop that runs an unknown number of iterations. Finally, A? is a test: the program that does nothing if A is true at the current state, and simply cannot execute if A is false.
The beauty of PDL is that we can prove all the reasoning patterns of Hoare logic from just four axiom schemas and a couple of rules. For instance, one axiom says: [α;β]A is equivalent to [α][β]A — “after doing α then β, A holds” means exactly “after α, you’re in a state from which every run of β leads to A.” Another crucial axiom handles loops: [α*]A ↔ (A ∧ [α][α*]A). It says that A is true after repeating α any number of times if and only if A is true now, and after doing α once, you’re in a state where repeating α again preserves A. This recursion-like pattern is what lets mathematical induction sneak into program proofs.
Logicians proved that PDL is sound (everything you can prove is true in all models) and complete (everything true in all models can be proved). And they showed that deciding whether a PDL formula is satisfied somewhere is solvable — though it takes exponential time in the worst case, which is actually not too bad for a logic that can describe arbitrary iterative computation.
Proving Programs Don’t Run Forever
Hoare’s original calculus dealt with partial correctness: a program might satisfy {A} α {B} simply because it never terminates at all, so it never reaches a bad state. A program that loops forever when A is true trivially satisfies any postcondition. For safety-critical software, that’s not good enough. We need total correctness: the program terminates, and when it does, B holds.
In PDL, if a program is deterministic, the diamond ⟨α⟩B already captures total correctness: there exists exactly one terminating run, and it ends in a B-state. But for non-deterministic or iterative programs, we need a way to say “can loop forever.” In 1982, Robert Streett extended PDL with a new proposition Δα, meaning “there is an infinite chain of α steps starting here.” With that, total correctness of a program α with precondition A and postcondition B becomes: A → (¬∞(α) ∧ [α]B), where ∞(α) is a predicate defined inductively — for atomic programs it’s false, for loops it’s true if there’s a repeating infinite path, etc. This logic, RPDL, can thus prove that a program both terminates and gives the right answer.
The good news: RPDL is still decidable, and its complexity — EXPTIME-complete — is the same as plain PDL, so adding termination reasoning doesn’t make the logic blow up horribly.
Why This Matters Every Time You Use an App
The next time you see a bug report, or your phone’s banking app reassures you that the connection is secure, remember: underneath that interface, someone might well have used ideas from dynamic logic to prove that a piece of code works for all possible inputs, not just the ones they tested. These techniques are used to verify critical systems — flight control software, medical devices, cryptographic protocols — where a mistake could cost lives.
Dynamic logic also opened doors to many cousins: adding the ability to reason backwards in time (CPDL), handling programs running in parallel (intersection), and even treating programs as games (Game Logic). All of these trace their lineage back to Pratt’s simple insight: programs are just relations between states, and modal logic is the perfect language to talk about them.
Proving a program correct might sound like a dry, academic exercise. But in a world where software runs everything from your school’s grading system to a Mars rover, having a logical guarantee — not just a hopeful test — is a superpower.
Think about it
- If a program passes ten thousand tests but nobody has a mathematical proof of its correctness, would you trust it to drive a car? What if it were a million tests?
- Can you ever be completely sure that a real computer will behave exactly like the logical model assumes? What might go differently?
- Imagine a logic that could prove your own reasoning is correct. Would you want to use it on your own thoughts? Why or why not?
