Nit: a unit test never proves that it works. At best it can prove that it doesn't work.

Otherwise, I agree.

Nit: "never"? Even if you unit test all cases?

How do you know you covered all cases. You can verify you cover all cases the code handles easily enough. However does the code actually handle all the cases that could exist? A formal proof can bring to your attention a case that you didn't handle at all.

Formal proofs also have limits. Donald Knuth once famously wrote "beware of bugs in the above code, I proved it correct but never ran it". Which is why I think we should write tests for code as well as formally prove it. (On the later I've never figured out how to prove my code - writing C++ I'm not sure if it is possible but I'd like to)

There are limited cases where this is possible. Like a pure function that takes a single 32bit number as input. Just go over all the possible inputs.

You can't as a verify all the outputs though, only that it doesn't crash, which isn't useful for detecting edge cases where the results are wrong but don't crash. And that is a single pure function, if that pure function with a wrong output is then fed into/used by some other function (a non-pure data storage in particular - a large part of what computers are used for is storage of some form, not pure functions) you can read off the end of the buffer or other bad things.

Even running through all 4 billion some cases a single 32 bit number can result in your test taking a significant amount of time - enough that you wouldn't want to run it very often. One value of real world tests is often that they can detect that you broke what you thought was a completely unrelated area of code.

Seriously? It is pretty easy to imagine function which has limited and low combinations count

Enums, bools, etc.

>can result in your test taking a significant amount of time - enough that you wouldn't want to run it very often.

It is irrelevant in theoretical discussions like this

Yes, never. You are assuming that the implementation of all unit test cases are themselves correct (that they would fail if there was any error in the case they cover). In fact unit tests are often wrong. In that context a unit test can't even prove code incorrect, unless we know that the unit test is correct.

IMO to prove that code is correct requires a proof; a unit test can only provide evidence suggestive of correctness.

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

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

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

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

That's what "exhaustive" means.