For a programmer, a proof separates two claims that sound similar but are not: “it works for the inputs I tried” and “it works for every input”. Testing gives you the first. A proof gives you the second.
A proof tells you what “every input” means without running every input. It also connects proof techniques to work you already do as a programmer. The proofs exercises on this site practice those techniques. This article explains the idea behind them.
Testing shows; proof guarantees
A test checks the cases you chose. A proof checks all of them at once - not by running anything, but by reasoning about the computation’s shape.
The Proofs exercises make that difference operational. Two oracles, two honest answers:
- Finite domain, confirm-by-enumeration. The oracle walks every element of the domain and checks the predicate. A pass is a genuine confirm: you inspected the whole set. That is as close as execution gets to a proof.
- Infinite domain, refute-only. The oracle samples. It can refute a false “for all” by finding a counterexample. It cannot confirm a true one, because leftover inputs remain. There is no “proved” verdict on this path. After a sample with no counterexample, a banner says testing is not proof. Read that banner. “No counterexample found” is not “proved”. Do not read “proved” on an infinite domain.
What a proof is made of
A proof is a finite chain of steps. Start with assumptions you accept. Justify each step with a rule you accept. If every step is legal, the conclusion cannot fail - not because you checked many examples, but because legal steps cannot lead from true assumptions to a false conclusion.
That is why the proof-order exercises on this site give you the steps and ask you to order them. The order is the logic: the assumption comes before the work, the work comes before the conclusion, and each step follows from what is already established. If you cannot order a proof step by step, you do not understand it.
For all, and there exists
Proofs are built from claims with two shapes:
- For all - the claim must hold for every element of a domain. One counterexample refutes it. If you prove a universal claim, you have covered inputs you will never see.
- There exists - the claim needs only one witness. One example proves it, and hunting for that one witness is often the whole game.
The quantifier exercises ask you to identify the shape of a claim and decide what would settle it.
The techniques, in programmer terms
The standard proof techniques are not a museum of math. Each is a mode of reasoning you already use. (The famous phrase “the proof is left as an exercise to the reader” is not really a joke; it is a job description. Someone has to do the work, and the textbook has moved on.)
-
Direct proof - trace the reasoning from assumption to conclusion, one justified step at a time. This is the trace exercises in miniature: you predict, step by step, what follows from what.
-
Proof by contraposition - to prove “if A then B”, prove “if not B then not A” instead; they are the same claim in disguise. The programmer version is proving an absence: to show a function never crashes on bad input, you prove that “input is bad” implies “the guard rejects it”.
-
Proof by contradiction - assume the opposite of what you want to prove, and show that assumption forces something impossible. The impossible conclusion is the failed test that proves the assumption was wrong. The classic example: assume a largest integer N exists; then N + 1 is a larger integer - contradiction, so no largest integer exists.
-
Proof by cases - split the domain into exhaustive cases and prove each one. This is pattern matching over every branch: if the cases cover everything and each case holds, the claim holds. The site’s proof that n(n+1) is always even splits on n being even or odd - every integer is one or the other, so the two cases cover everything.
-
Induction - the one that matters most for a programmer. To prove a claim for every natural number, prove it for 0, and prove that whenever it holds for k, it holds for k + 1. That is a recursive function: a base case and a recursive step. Every recursive function you trust is secretly an inductive proof - the base case is the base case, and the recursive call works because you are proving the claim for a smaller input.
Invariants are inductive claims in disguise
A loop is correct when an invariant holds at the start, survives every iteration, and implies the answer at the end. That is induction: the invariant holds at the base, the loop body is the inductive step, and the final state is the conclusion. When you reason about why a loop terminates or why a recursive function returns the right answer, you are doing a proof, whether or not you call it one.
What is not a proof
- Examples - however many. Ten thousand passing tests still leave input 10,001 unchecked.
- Authority - “it is known to be true” is not a chain of steps you can follow.
- No counterexample found - the absence of a failure is not a guarantee, which is exactly what the site’s honesty banner says.
- Intuition - valuable for finding the proof, but the proof is the chain that checks the intuition.
Why this matters here
Everything on this site depends on the difference in this article. The trace exercises teach you to predict what code does, one step at a time - that is direct reasoning, the raw material of a proof. The proofs exercises at /proofs practice the techniques on small, complete claims. Induction is the keystone of the path: it is the proof technique that says “every natural number”, and it has the same shape as the recursion you write. The reasoning replays show a strong solver doing this under time pressure: stating a hypothesis, hunting a counterexample, pivoting on a demonstrated failure.
Proofs are not an obstacle between you and the algorithms. They let you know that what you built works for everything. That is the same skill you use when you write a recursive function and trust it.
Where to go next
- Proofs - structured proofs and quantifiers, with the honesty banner on infinite domains: confirm-by-enumeration when the domain is finite, refute-only when it is not.
- How to read a proof exercise - this article’s ideas as an actual exercise: the mechanics of stating, structuring, and checking a claim.
-
Induction: the proof pattern recursion already uses
- the keystone technique this article’s closing names: “every natural number”, and why a recursive function is the same shape.