The trouble with "it passed"
You have written a small algorithm — say, one that finds the largest number in a list. You feed it a handful of lists, eyeball the answers, and they all look right. Done? It is tempting to say yes. But pause on what you actually checked: you confirmed the method gives the right answer on the specific inputs you happened to try. The question we really care about is different and much bigger: does it give the right answer on every valid input? That gap — between "works on what I tried" and "works on everything" — is the whole reason this rung exists.
The trouble is arithmetic. A list of 20 small integers already has astronomically many possibilities; a method that takes arbitrary-length input has infinitely many. No finite pile of tests, however large, can cover an infinite space of inputs. So a test suite can only ever do one of two things: catch a bug, or fail to catch one. It can prove your algorithm wrong (one failing case is enough), but it can never prove it right. This asymmetry is the single most important idea in the rung, and it is captured by the term correctness, not plausibility.
What a proof gives you that tests cannot
A correctness argument is a piece of reasoning that covers all inputs at once, not one at a time. Instead of running the algorithm on input number 1, then 2, then 3, you reason about the structure of the algorithm itself — its loops, its recursion, the relationships it maintains — and show that whatever the input, the answer it returns must satisfy what the problem asks for. One careful argument retires the whole infinite test suite. That is exactly what we mean by algorithm correctness: not "I have not yet found a counterexample", but "there is no counterexample, and here is why".
Think of the difference physically. Testing is like checking that a bridge holds by driving a few trucks across it and noting it did not fall. A proof is like the structural calculation showing the bridge holds for every load up to its rated limit — including loads no one drove across yet. The calculation does not replace the trucks (you still test!), but only the calculation lets you say something true about loads you never tried. In code, the "loads you never tried" are the inputs that will arrive next year, from users you have not met, in combinations you did not imagine.
Two halves of a correct algorithm
When we say an algorithm is correct, we are quietly making two separate promises, and it pays to pull them apart. The first is: if the algorithm halts, the answer it produces is right. The second is: it actually does halt — it never runs forever. The first promise alone is called partial correctness; the two promises together are total correctness. This split is the term partial versus total correctness, and confusing the two is a classic mistake.
Why bother splitting them? Because they are proved by completely different tools, and you will meet both later in this rung. The "answer is right" half is established with a loop invariant (a property kept true on every pass) backed by mathematical induction. The "it halts" half needs a separate argument: you find some quantity that strictly decreases on every step and cannot decrease forever — this is termination via a decreasing measure. An algorithm can be partially correct yet loop forever on some input; that is still a bug, just a different kind, and only the termination argument catches it.
Naming the goalposts: pre- and postconditions
Before you can prove an algorithm "correct", you have to pin down what correct means for it — otherwise the word floats free. We do that with two statements. A precondition says what the caller promises to hand in ("the input is a list of integers", "the array is already sorted", "n is at least 1"). A postcondition says what the algorithm promises to deliver if that input was honored ("the output is the largest element", "the array comes back sorted"). Together they form the contract named by preconditions and postconditions.
This contract is not bureaucracy — it is what makes a correctness claim checkable. "Binary search is correct" is meaningless until you add the precondition "the array is sorted". Feed binary search an unsorted array and it may return garbage; that is not a bug in binary search, because the caller broke the contract. Stating the precondition tells you precisely which inputs you owe a correct answer on, and which you are entitled to ignore. Every proof in this rung will quietly begin by assuming the precondition and end by establishing the postcondition.
{ precondition } <-- what we may assume about the input
ALGORITHM
{ postcondition } <-- what we must guarantee about the output
PROVE: precondition ==> algorithm halts AND postcondition holdsWhere intuition lies to you
If tests cannot prove correctness, you might hope a confident hand-wave can — "just look at it, obviously it works". Sometimes that hunch is right. Often it is exactly where bugs hide, because plausible-looking reasoning skips the case that breaks. Consider a routine that searches for an item by repeatedly halving a range: it feels obviously right, yet the boundary arithmetic (does the range include both endpoints? do you go to `mid` or `mid+1`?) is famously easy to get subtly wrong, looping forever or missing the target on a handful of inputs. "Looks locally fine" is not a proof — a theme you will see again with greedy algorithms, where a locally best choice can fail to be globally best.
Notice too that even a statistical sense of "usually fine" is the wrong target. The behavior of an algorithm depends on which input you give it, and the worst, best, and average case can be wildly different. A method that is correct on 99.9% of inputs and silently wrong on the rest is not a correct algorithm — it is a bug that is hard to find. Correctness is an all-inputs claim, with no exceptions hiding in the long tail. That is precisely why we trade the comfort of "it usually works" for the harder, sturdier currency of proof.
- State the contract: write down the precondition (what you assume) and the postcondition (what you must guarantee).
- Prove partial correctness: find a loop invariant and use induction to show the postcondition holds whenever the algorithm stops.
- Prove termination: exhibit a measure that strictly decreases each step and cannot fall forever, so the algorithm must stop.
- Conclude total correctness: partial correctness plus termination together mean the algorithm always halts with the right answer.
So why test at all?
None of this means "stop testing" — testing and proving are partners, not rivals. Tests catch the things proofs do not: a typo, a mismatch between the algorithm on paper and the code on the machine, a misread library, a precondition the real world quietly violates. A proof reasons about an idealized algorithm; tests check the messy implementation of it. Most of the time you will reach for tests first because they are fast and cheap, and reserve a full proof for the load-bearing core where a hidden error would be catastrophic.
The right mindset is to let each method do what it is good at. A proof gives you the universal guarantee — true for all inputs, by reason — that no amount of testing can ever supply. Testing gives you a reality check against the gap between your reasoning and your running code. The rest of this rung builds the proof half of that partnership, one tool at a time: first the loop invariant, then induction, then termination, and finally two full worked proofs you can imitate. By the end, "I argued it, and here is the argument" will feel as natural as "I ran it, and it looked right".