> Great! Now I have a stupid bug that always returns 0, so these all pass, and since I didn't think about this case (otherwise I'd not have written that stupid bug in the first place), I didn't add a property about a + b only being 0 if a == -b and boom, test is happy, and there is nothing that the framework can do about it.

Well, just add one example based test for eg 1 + 2 = 3, and you would catch this bug.

You can freely mix and match property based tests with example based tests.

> Coming up with those properties is hard for real life code and my main gripe with formal methods based approaches too, like model checking or deductice proofs.

Yes, property based testing is an acquired skill that has to be learned.

It's not so bad, once you've done it a few times, though.

It also changes how you design code in the first place. Just like even example-based testing changes how you design your code.

> They move the bugs from the (complicated) code to the list of properties, which ends up just as complicated and error prone, and is entirely un...tested.

You might be doing this wrong, if your list of properties is as complicated as the code. And it's not 'untested': you are exercising your properties against your code.

For a conceptually really simple example: suppose you have two different ways to solve a certain problem, and suppose neither is really simpler than the other. You still gain something from comparing the output of both approaches on random input: unless you made the mistake in both approaches, many bugs will show up as discrepancies that you can investigate. Hypothesis even includes 'shrinking' to helpfully provide you with a minimal counterexample that shows the divergence.

From a formal point of view, you can say that this property is 'untested'; but in practice you still gain something by comparing the two implementations.