Comment by teiferer
13 hours ago
> a + b == b + a
> a + (b + c) = (a + b) + c
> a + (-a) == 0
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.
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. 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.
Contrast that with an explicit dead-simple test. Test code doesn't have tests. It needs to be orders of magnitudes simpler than the system it's testing. Its correctness must be obvious. Yes, it is really hard to write a good test. So hard that it should steer how you architect your system under test and how you write code. How can I test this to have confidence that it's correct? That must be a guiding principle from the first line of code. Just doing this as an afterthought by playing lottery and trying to come up with smart properties after the fact is not going to get you the best outcome.
For the example it would be easily caught with PBT by testing the left and right identities for addition.
In general though, the advice is don't excessively dogmatic. If you can't devise a property to test, use traditional testing with examples. It's not that hard. Same way to deal with the problem of end-to-end tests or unit tests not being useful for certain things, use the appropriate test style and approach to your problem.