[planede]

Mistakes in proofs are just as probable as mistakes in exhaustive tests.

An exhaustive test is just one type of a machine verified proof.

[nicoburns]

> An exhaustive test is just one type of a machine verified proof.

Not entirely sure I agree with this. A proof by construction is a very different beast to empirical unit tests that only cover a subset of inputs. The equivalent would be units tests that cover every single possible input.

[planede]

> The equivalent would be units tests that cover every single possible input.

That's what "exhaustive" means.