That’s not the case! Perhaps you’re thinking in QuickCheck? Those are different. QuickCheck creates millions of random unit tests for you based on a specification. Formal proofs are a different beast: you mathematically prove the specification is correct. That is, suppose you want to prove that the function f(x) = 2 * x, when given a natural number, returns an even number. The unit test way would write a bunch of tests:
assert(f(7) % 2 == 0)
assert(f(3) % 2 == 0)
assert(f(5) % 2 == 0)
assert(f(9) % 2 == 0)
assert(f(0) % 2 == 0)The QuickCheck way would do the same thing, but instead would generate the tests automatically. The formal proof, instead, would be this:
proof : ∀ (n : Nat) -> f(n) % 2 = 0
proof = let n be any natural number:
assume n = 0. then,
f(0) % 2 = 0 % 0 = 0.
assume n = k+1. then,
f(k+1) % 2 = 2*(1+k)%2 = (2+2*k)%2 = 2*k % 2 = f(k) % 2
but, from induction hypothesis, f(k) % 2 = 0
thus, f(k+1) % 2 = 0That is, first you observe that the property holds for f(0). Then you check if, by assuming it holds fork, it holds for k+1. If that is the case, then it must be that f holds for every number. That is a very simple inductive proof. Languages featuring theorem proving are capable of checking those proofs, thus, unlike tests, they cover an infinite amount of inputs.
