[pclowes]

Interesting, could you show me a formal proof that can't be expressed in logic (ie. code) and then tested?

My thought here is that since proofs are logic and so is code you can't have a proof that can't be represented in code. Now admittedly this might look very different than typical say JUnit unit tests but it would still be a test validating logic. I am not saying every system is easily testable or deterministic but overall, all else equal, the more tested and testable a system is the better it is.

IME things that are very hard to test are often just poorly designed.

[aljgz]

Consider a function that gets an array of integers and a positive number, and returns the sum of the array elements modulo the number. How can we prove using tests, that this always works for all possible values?

Not discounting the value of tests: we throw a bunch of general and corner cases at the function, and they will ring the alarm if in the future any change to the function breaks any of those.

But they don't prove it's correct for all possible inputs.

[pclowes]

I would lean towards types and property testing here using tools like Coq.

[aljgz]

Can you elaborate?

[layer8]

Tests can generally only test particular inputs and/or particular external states and events. A proof abstracts over all possible inputs, states, and events. It proves that the program does what it is supposed to do regardless of any particular input, state, or events. Tests, on the other hand, usually aren't exhaustive, unless it's something like testing a pure function taking a single 32-bit input, in which case you can actually test its correctness for all 2^32 possible inputs (after you convinced yourself that it's truly a pure function that only depends on its input, which is itself a form of proof). But 99.99% of code that you want to be correct isn’t like that.

As an example, take a sorting procedure that sorts an arbitrarily long list of arbitrarily long strings. You can't establish just through testing that it will produce a correctly sorted output for all possible inputs, because the set of possible inputs is unbounded. An algorithmic proof, on the other hand, can establish that.

That is the crucial difference between reasoning about code versus merely testing code.

[pclowes]

I agree with that but I would say that if I required formal verification of that kind I would move the proof based rationale into the type system to provide those checks.

I would add Tests can be probabilistically exhaustive (eg property based testing) and answer questions beyond what proof based reasoning can provide ie. is this sorting of arbitrary strings efficient and fast?

[joseneca]

Proofs are arguably still better than tests at evaluating efficiency, at least for smaller components/algorithms in isolation. While there are cases where constant factors that can't be described well in a proof matter, in most cases, the crucial element of an algorithm's efficiency lies in how the complexity scales, which can be proven in the vast majority of cases. On the other hand, relying solely on benchmarking introduces a lot of noise that can be difficult to sort through.