Comment by chriswarbo

> 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.

This sounds backwards to me. How could you write any tests, or indeed implement any functions, if you don't know any relationships between the arguments/return-value, or the state before/after, or how it relates to other functions, etc.?

For the addition example, let's say the implementation includes a line like `if (x == 0) return y`; would you seriously suggest that somebody writing that line doesn't know a property like `0 + a == a`? Would that only be "an afterthought" when "trying to come up with smart properties after the fact"? On the contrary, I would say that property came first, and steered how the code was written.

Incidentally, that property would also catch your "always returns 0" counterexample.

I also don't buy your distinction that "real life code" makes things much harder. For example, here's another simple property:

    delete(key); assert lookup(key) == []

This is pretty similar to the `a + (-a) == 0` example, but it applies to basically any database; from in-memory assoc-lists and HashMaps, all the way to high-performance, massively-engineered CloudScale™ distributed systems. Again, I struggle to imagine anybody implementing a `delete` function who doesn't know this property; indeed, I would say that's what deletion means. It's backwards to characterise such things as "com[ing] up with smart properties after the fact".