Victor Maia
Aug 31, 2018 · 1 min read

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 = 0

That 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.

    Victor Maia

    Written by

    aaaaa

    Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
    Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
    Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade