Algorithm Correctness

Intro to Proofs · Axiom Academy

Your sorting code passes every test you throw at it — but there are infinitely many inputs. Mathematical induction proves it works for all of them. You can't test every array — there are 10 , 1,000 , a million -element inputs, endlessly many. So instead of testing, you prove — and the engine behind that proof is induction. Insertion sort walks left to right. Step through it: after it processes position i , the cells arr[0…i] are always sorted. That standing-true property is the loop invariant — drag to watch it hold. Assume the first k cells are already sorted (the inductive hypothesis). Now insert one more element. Drag its value to anything — it shifts the larger cells right and drops into place, and the first k+1 cells stay sorted. One step proves them all. Base case: it works for size 1. The step: size k → size k+1 . Chain them and the dominoes fall — 1 topples 2, 2 topples 3, forever. Drag how far you want to go: two proofs cover infinitely many input sizes. Two steps — base case and k → k+1 — replace infinitely many tests. This is formal verification : the same reasoning that proves flight software, encryption, and pacemaker code correct for every input, not just the ones anyone happened to try.

This is the written version of the interactive lesson above. See the full Intro to Proofs course.