Introduction

Every programmer has stared at a bug that passed all the tests yet destroyed production. Testing shows the presence of bugs; it cannot prove their absence. In 1969, computer scientist Tony Hoare published a two-page paper that took a radically different approach: treat programs as mathematical objects and prove they are correct.

The core idea is a Hoare triple, written {P} C {Q}:

  • P is the pre-condition — what must be true before command C runs.
  • C is the command (an assignment, a loop, a sequence of statements).
  • Q is the post-condition — what is guaranteed to be true after C finishes.

If you can prove the triple is valid, you don't need to test: the program is mathematically correct relative to that specification. The sum-to-n loop that adds 1 + 2 + … + n? You prove it with a loop invariant — a property that holds before every iteration and implies the result when the loop exits.

This isn't just academic elegance. The same formalism, extended to separation logic and machine-checked proofs, powered the complete formal verification of the seL4 microkernel (2009) — the first operating-system kernel proved correct for every possible input. Hoare logic sits at the foundation of program verification tools, proof assistants, and the correctness guarantees built into safety-critical software worldwide.

Try It: Verify a Loop

The classic example is summing 1 + 2 + … + n. Here is the loop in pseudocode:

{ n ≥ 0 }
i := 0; s := 0
while i < n do
  i := i + 1
  s := s + i
{ s = n*(n+1)/2 }

The loop invariant s = i*(i+1)/2 AND i ≤ n is the key: it holds before the first iteration (when i = 0, s = 0) and is preserved by every step. When the loop exits (i = n), the invariant plus the exit condition give you the post-condition.

<div class="layout">
  <div class="left-col">
    <div class="pseudo">
      <div class="pseudo-line pre" id="line-pre"><span class="brace">{</span> n &ge; 0 <span class="brace">}</span></div>
      <div class="pseudo-line" id="line-init">i := 0 &nbsp; s := 0</div>
      <div class="pseudo-line loop-kw" id="line-while"><b>while</b> i &lt; n <b>do</b></div>
      <div class="pseudo-line indent" id="line-i">&nbsp;&nbsp;i := i + 1</div>
      <div class="pseudo-line indent" id="line-s">&nbsp;&nbsp;s := s + i</div>
      <div class="pseudo-line post" id="line-post"><span class="brace">{</span> s = n&middot;(n+1)/2 <span class="brace">}</span></div>
    </div>
    <div class="controls">
      <label>n = <input id="nval" type="number" min="0" max="10" value="4" style="width:3.5rem"></label>
      <button id="btnStep" type="button">Step</button>
      <button id="btnRun" type="button">Run all</button>
      <button id="btnReset" type="button" class="ghost">Reset</button>
    </div>
  </div>
  <div class="right-col">
    <div class="panel">
      <div class="panel-title">Current state</div>
      <table id="stateTable">
        <tr><td>n</td><td id="sv-n">4</td></tr>
        <tr><td>i</td><td id="sv-i">0</td></tr>
        <tr><td>s</td><td id="sv-s">0</td></tr>
      </table>
      <div class="inv-box" id="invBox">
        <div class="inv-label">Loop invariant</div>
        <div class="inv-formula">s = i&middot;(i+1)/2 &nbsp;&amp;&nbsp; i &le; n</div>
        <div class="inv-status" id="invStatus">—</div>
      </div>
      <div class="post-box" id="postBox" style="display:none">
        <div class="inv-label">Post-condition</div>
        <div class="inv-formula">s = n&middot;(n+1)/2</div>
        <div class="inv-status" id="postStatus">—</div>
      </div>
      <div class="msg" id="msg"></div>
    </div>
  </div>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.layout { display: flex; gap: 1rem; align-items: flex-start; flex-wrap: wrap; }
.left-col { flex: 1 1 260px; }
.right-col { flex: 1 1 220px; }
.pseudo { background: #1e2430; color: #cdd6f4; border-radius: 10px; padding: .8rem 1rem;
          font: 13px/1.7 ui-monospace, monospace; margin-bottom: .8rem; }
.pseudo-line { border-radius: 5px; padding: 0 4px; transition: background .2s; }
.pseudo-line.active { background: #3a4459; }
.brace { color: #89b4fa; font-weight: 700; }
.pre, .post { color: #a6e3a1; }
.loop-kw { color: #cba6f7; }
.indent { color: #f5c2e7; }
.controls { display: flex; gap: .5rem; flex-wrap: wrap; align-items: center; margin-top: .3rem; }
label { font-size: .9rem; }
input[type=number] { border: 1px solid #aaa; border-radius: 6px; padding: 2px 4px; }
button { font: 600 13px system-ui; padding: .4rem .8rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.panel { background: #f4f6f9; border: 1px solid #dde3ea; border-radius: 10px; padding: .8rem 1rem; }
.panel-title { font-weight: 700; font-size: .85rem; color: #555; margin-bottom: .5rem; }
#stateTable td { padding: 2px 8px; font: 14px ui-monospace, monospace; }
#stateTable td:first-child { color: #555; }
.inv-box, .post-box { margin-top: .7rem; background: #fff; border: 1px solid #dde3ea;
                      border-radius: 8px; padding: .5rem .7rem; }
.inv-label { font-size: .75rem; color: #888; font-weight: 600; text-transform: uppercase; letter-spacing: .04em; }
.inv-formula { font: 13px ui-monospace, monospace; color: #333; margin: 2px 0; }
.inv-status { font-size: .85rem; font-weight: 700; min-height: 1.2em; }
.inv-status.ok { color: #0a7d33; }
.inv-status.bad { color: #c92f3c; }
.inv-status.neutral { color: #888; }
.msg { margin-top: .6rem; font-size: .85rem; font-weight: 600; min-height: 1.3em; color: #1d3557; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Hoare triple demo: verify the sum-to-n loop step by step.
// Triple: { n>=0 } i:=0; s:=0; while i<n do { i:=i+1; s:=s+i } { s=n*(n+1)/2 }
// Loop invariant: s = i*(i+1)/2  AND  i <= n
//
// Steps:
//  0: highlight pre-condition  (trivially satisfied for n>=0)
//  1: init i=0, s=0
//  2...: each loop body execution
//  final: exit condition + post-condition check

let n, i, s, phase; // phase: 'pre'|'init'|'body'|'done'

function getN() {
  const v = parseInt(document.getElementById('nval').value, 10);
  return isNaN(v) || v < 0 ? 0 : Math.min(v, 10);
}

function reset() {
  n = getN();
  i = 0; s = 0; phase = 'pre';
  clearHighlights();
  highlight('line-pre');
  updateState();
  setMsg('Pre-condition: n ≥ 0. Ready to initialize.');
  document.getElementById('postBox').style.display = 'none';
  setInv('neutral', '— (before loop starts)');
  setPost('neutral', '—');
  document.getElementById('btnStep').disabled = false;
  document.getElementById('btnRun').disabled = false;
}

function highlight(id) {
  document.querySelectorAll('.pseudo-line').forEach(el => el.classList.remove('active'));
  const el = document.getElementById(id);
  if (el) el.classList.add('active');
}
function clearHighlights() {
  document.querySelectorAll('.pseudo-line').forEach(el => el.classList.remove('active'));
}

function updateState() {
  document.getElementById('sv-n').textContent = n;
  document.getElementById('sv-i').textContent = i;
  document.getElementById('sv-s').textContent = s;
}

function invariantHolds() {
  return s === i * (i + 1) / 2 && i <= n;
}

function setInv(cls, msg) {
  const el = document.getElementById('invStatus');
  el.className = 'inv-status ' + cls;
  el.textContent = msg;
}

function setPost(cls, msg) {
  const el = document.getElementById('postStatus');
  el.className = 'inv-status ' + cls;
  el.textContent = msg;
}

function setMsg(txt) {
  document.getElementById('msg').textContent = txt;
}

function step() {
  if (phase === 'pre') {
    // init
    i = 0; s = 0; phase = 'init';
    highlight('line-init');
    updateState();
    setInv('ok', '✔ s=0=0⋅0⋅1/2, i=0≤0≤n');
    setMsg('Initialized i=0, s=0. Invariant holds.');
    return;
  }
  if (phase === 'init') {
    // decide: enter loop or skip
    if (i < n) {
      phase = 'body';
      highlight('line-while');
      setMsg(fmt('Condition i=%i% < n=%n% is TRUE → entering loop body.', { i: i, n: n }));
    } else {
      phase = 'done';
      finish();
    }
    return;
  }
  if (phase === 'body') {
    // execute one body iteration
    i = i + 1;
    highlight('line-i');
    updateState();
    setMsg(fmt('i := i + 1 → i = %i%', { i: i }));
    // s update will be next sub-step; simplify: do both at once
    s = s + i;
    highlight('line-s');
    updateState();
    const ok = invariantHolds();
    if (ok) {
      setInv('ok', '✔ s=' + s + '=' + i + '⋅' + (i+1) + '/2=' + (i*(i+1)/2));
    } else {
      setInv('bad', '✘ invariant violated!');
    }
    setMsg(fmt('After iteration %i%: i=%i%, s=%s%. Invariant: %v%', { i: i, s: s, v: ok?'OK':'BROKEN' }));
    // check loop guard again
    if (i < n) {
      highlight('line-while');
    } else {
      phase = 'done';
      finish();
    }
    return;
  }
}

function finish() {
  highlight('line-post');
  document.getElementById('postBox').style.display = 'block';
  const expected = n * (n + 1) / 2;
  const ok = s === expected;
  setPost(ok ? 'ok' : 'bad',
    ok ? '✔ s=' + s + '=n⋅(n+1)/2' : '✘ s=' + s + '≠' + expected);
  setMsg(ok
    ? fmt('Loop exited with i=n=%n%. Post-condition holds! s=%s%=%n%⋅%n%%v%/2', { n: n, s: s, v: 1 })
    : 'ERROR: post-condition violated (should never happen for correct n≥0).');
  document.getElementById('btnStep').disabled = true;
  document.getElementById('btnRun').disabled = true;
}

function runAll() {
  document.getElementById('btnStep').disabled = true;
  document.getElementById('btnRun').disabled = true;
  let ticks = 0;
  const maxTicks = 100;
  function tick() {
    if (phase === 'done' || ticks > maxTicks) return;
    step();
    ticks++;
    if (phase !== 'done') setTimeout(tick, 180);
  }
  tick();
}

document.getElementById('btnStep').addEventListener('click', step);
document.getElementById('btnRun').addEventListener('click', runAll);
document.getElementById('btnReset').addEventListener('click', reset);
document.getElementById('nval').addEventListener('change', reset);

reset();

// Self-test: verify invariant holds throughout for n=0..6
(function selfTest() {
  for (let testN = 0; testN <= 6; testN++) {
    let ii = 0, ss = 0;
    // invariant before loop
    console.assert(ss === ii*(ii+1)/2 && ii <= testN, 'inv pre n=' + testN);
    while (ii < testN) {
      ii++; ss += ii;
      console.assert(ss === ii*(ii+1)/2 && ii <= testN, 'inv body n=' + testN + ' i=' + ii);
    }
    console.assert(ss === testN*(testN+1)/2, 'post n=' + testN);
  }
  console.log('Self-test: invariant and post-condition verified for n=0..6');
})();
Result
Console

Use the Step button to advance one iteration at a time. The panel on the right shows the current state and highlights whether the invariant holds. Press Run all to execute to completion, or Reset to start over. Notice how the invariant s = i*(i+1)/2 stays green through every step — that is the proof.

The Real Complexity

Hoare logic is a clean, elegant proof system — but it doesn't come for free.

  • Soundness: if a triple {P} C {Q} is provable in the system, it is genuinely true. No false proofs slip through.
  • Relative completeness (Cook, 1978): any true triple can be proved — provided you can express every invariant in the assertion language. Stephen Cook showed this by reducing to arithmetic expressibility.
  • The bottleneck is invariant synthesis. Finding a loop invariant is not mechanical: in general, computing the weakest pre-condition for an arbitrary program is undecidable (it reduces to the halting problem). Human experts or automated tools must guess or search for invariants.
  • Scalability: hand-proofs explode with program size. Modern tools like Frama-C, VeriFast, and Dafny automate much of the reasoning, but verifying a full system — like seL4's 10 000-line kernel — required years of human effort.
  • Total vs partial correctness: the basic triple only guarantees the result if the program terminates. Proving termination (that loops always exit) is a separate, also undecidable problem in general.

So Hoare logic occupies a precise niche: a complete formal foundation for what correctness means, paired with the hard practical reality that finding the proofs requires ingenuity the system cannot supply automatically. It is the theoretical bedrock; program synthesis and automated invariant discovery are the open frontier built on top.

Where It Matters

The formalism Hoare invented in 1969 now underlies some of the most consequential software ever built:

  • seL4 verified kernel: the 2009 proof (Gerwin Klein et al., NICTA/UNSW) showed, in the Isabelle proof assistant, that the microkernel's C implementation matches its abstract specification for all possible inputs — the first such proof for an OS kernel. It uses a descendant of Hoare logic extended to handle low-level memory.
  • Separation logic (John Reynolds, 2002): extends Hoare triples with a separating conjunction P * Q, allowing local reasoning about disjoint pieces of heap. This made heap-manipulating programs — linked lists, trees, dynamic allocation — tractable to verify. Facebook's Infer static analyser is built on bi-abduction, a separation-logic technique.
  • Rust's borrow checker: while not literally Hoare triples, Rust's ownership and lifetime system encodes spatial separation invariants that rule out data races and use-after-free at compile time — the same intuition separation logic formalises.
  • Proof assistants and verified compilers: Coq and Isabelle host Hoare-logic-style reasoning; CompCert, a formally verified C compiler, uses it to guarantee that optimisations never change program meaning.
  • Smart contracts and cryptography: high-value Ethereum contracts are now routinely verified using tools like Certora Prover and K framework, both rooted in axiomatic semantics.

Anywhere a bug costs lives or billions of dollars — aerospace, medical devices, financial infrastructure — the question Hoare posed in 1969 is still the right one: can you prove it correct?

Conclusion

Tony Hoare's two-page paper introduced an idea with permanent force: a program is not just code that runs — it is a mathematical statement that can be proved or refuted. The triple {P} C {Q} gave computer science a precise language for saying what a program must do and demonstrating it holds for every possible input, not just the ones you thought to test.

The limits are real. Finding loop invariants is undecidable. Proofs of large systems require enormous human effort. But those limits define the frontier, not a ceiling: separation logic, automated invariant synthesis, and machine-checked proof assistants keep pushing what is verifiable in practice.

The next time a critical system ships with a mathematical correctness certificate — a verified kernel, a proved cryptographic library, a compiler that guarantees it never miscompiles — remember the source: a 1969 insight that programs and proofs are the same thing, separated only by the effort required to write them down. See also program synthesis and the halting problem for the boundaries that make this effort so hard.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/hoare-logic/Content licensed under CC BY-NC 4.0.