Why Property Testing Finds Bugs Unit Testing Does Not (2021)

I would love to used PBT more, but many tests I write have only one answer per input. Think sum like aggregations.

For then it's not clear how would one derive the answer from the generated inputs, that is what code is for.

But PBT can be great for pruning out crashes you don't expect while parsing.

> The majority of errors you find with testing are either issues with an entire "partition" of inputs or "boundary" inputs, like INT_MIN.

I don't find this to be true at all. Most bugs I find are business scenarios that I didn't consider or mismatches in API expectations etc. Rarely is a bug for me coming from not considering edge cases of min and maximum values for integers, floats etc.

Update: It’s actually been divided into multiple sections; if your code assumes a single section, it will break as of the addition of multibyte characters in Unicode v7.1

Multiple problems.

Proving code is only as good as the requirements which are often garbage - the customer often doesn't know what they even want. Even if you put in effort, requirements as the proof needs are often very abstract from the customer requirements and so your program can be proved but still be wrong because it doesn't do what the customer really wanted. In any complex program is a reasonable to state that several requirements are wrong and thus even if your prove your code correct it will be wrong. Often the problem itself cannot even be formally defined - a spell checker cannot be proved correct because human languages are not formally defined, not that you can't prove one, just that whatever you prove will be wrong.

Many systems are very complex. You can (should!) prove simple algorithms, but put everything together and a proof is not something we can do at all. There are too many halting problems like things in large programs.

Tests solve some of the above problems: They can (do not confuse with what they do!) be a simple example of "yes when inputs are exactly x,y,z then I expect that result". A bunch of simple examples that make sense can often be close enough.

We do a lot more theorem proving than most people realize. Types which many languages have are a form of formal proof. They don't cover everything, but even in C++ they cover a lot of issues.

I think the best answer is a combination: prove the things we know how to prove, and test the rest and hope that between the two we have covered enough to prevent bugs.

> I would love to used PBT more, but many tests I write have only one answer per input. Think sum like aggregations.

Not quite sure what you mean by "only one answer per input" (that it's a function, i.e. a 1:1 mapping?), but there are of lots of properties that aggregations might typically need to satisfy, e.g. off the top of my head:

    # Identity element
    forAll(pre, post) {
      assertEqual(
        agg(pre ++ [agg([])] ++ post),
        agg(pre ++ post)
      )
    }

    # Invariant to order
    forAll(elems, seed) {
      assertEqual(
        agg(elems),
        agg(permute(elems, seed))
      )
    }

    # Left-associative
    forAll(xs, ys, zs) {
      assertEqual(
        agg([agg(xs ++ ys)] ++ zs),
        agg(xs ++ ys ++ zs)
      )
    }

    # Right-associative
    forAll(xs, ys, zs) {
      assertEqual(
        agg(xs ++ [agg(yz ++ zs)]),
        agg(xs ++ ys ++ zs)
      )
    }

(FYI these typical properties of a (commutative) monoid, which is an algebraic structure that describes many "aggregation-like" operations)