Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?

All this is just a roundabout way of saying I don't write unit tests. There is no value in it when I have convinced myself each subcomponent is correct and that composition of those subcomponents preserves correctness. You can write all the unit tests in the world and if you don't verify that the composition of your components preserves the correctness properties those tests are meant to verify then you might as well not have written those tests because now you have created a false sense of security.

If you can verify the kernel pieces of your code and then the composition mechanisms then you're done. You don't need to verify the entire thing as long as the entire thing is built with the kernel pieces and verified composition mechanisms that preserve correctness.

I also suspect we are still talking about separate classes of software. For your run of the mill twitter clone if it makes the corporate overlords happy then write as many unit tests as you want because it doesn't make a difference either way. But if we're talking about actual fundamental software like OS kernels and compilers then I don't think you can have enough formal verification.

Your test is intended to convey to the reader that your function does addition and provide an example of how to access that function. The functional part of the test is to verify that your claim is true, rather than the stories of yore when the documentation often didn't match what the code actually did.

As a nice side effect, when you refactor your function in the future and you mistakenly turn it into multiplication, the test will give you a sanity check that you meant for it to do addition. Perhaps not a big deal in your contrived example, but is huge in the real world where functions are not quite so simple.

Testing is not for verifying a function is mathematically correct.

> If you're going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?

At the moment this "a bit further" is a bit like saying if you don't like the price of milk at your corner store, why don't you go to a farm to get a quart? Sure, you might be able to do that, but it's not exactly a comparable effort.

> Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z?

I gained some evidence. Do you refuse to accept the theory of gravity because we've only measured some examples where F Gm_1m_2 / r^2, not proven it from first principles?

Yeah, but unit testing suites don't actually reason inductively. Scientists do. Big difference.

> Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?

One could take the middle road and express commutativity, distributivity etc. through invariants and use a fuzzy testing tool to generate tests for it. Generating 100 tests sounds a lot better than a single handwritten one, though of course it's not as good as actually proving it for all inputs.