I brought in the QuickTheories[0] library for property testing at work after being exposed to the articles here[1] (the final rule test is particularly interesting). My first use case was to test a generated parser for a restricted subset of the grammar for content security policy URLs, but I think this might be a bad use case since I'm not exactly testing "properties" so much as using the system for test data generation and quick code coverage. e.g. I have a test called something like testUrlPaths() that's mostly exercising the parser to make sure it doesn't forbid a valid but strange URL path that someone could enter. However while writing that test I discovered the parser was really doing the right thing, I found some violations with paths containing a '%' but not two hex digits immediately following. Unless I was writing unit tests for every bit of the grammar and paid attention to that part, I doubt I would have thought to test for them myself... Maybe the happy path of '%20' but not the fact that '%2' should be invalid. In the end I extracted those cases into three specific tests that will be there in case someone gets the funny idea to replace the validator with something not generated from a grammar (or generated from the wrong grammar), which isn't that unlikely since the spec allows for a lot more than what one might naturally consider allowing on your own (e.g. ftp resources).

Like with certain kinds of unit testing, I have the sense that the process of using a property testing framework has beneficial effects while a system is under development which aren't exactly clear to see from the artifacts of the final committed code and tests since by then you've dealt with a bunch of edge cases the tests told you about and have refactored / rewrote / removed things. So try it! Even if you don't commit it. And anyway the "trivial" problems are still worthwhile too (like catching errors in a pair of serializer/deserializer classes for some custom data), and like other kinds of tests it's best for your properties to be short and easy to read.

I think the chief difficulty is just adjusting to thinking in terms of "properties" that are worthwhile to check. The examples here[2] (and summarized in the quicktheories readme) are good starting points. Also it's more on the toy example side but I've personally made an analogy to Polya's How to Solve It introductory problem of finding the diagonal length of a box. He lists a bunch of other mathematically interesting things you can do with the solution besides just use it to solve the one problem, and most of those things could be encoded into properties. (Like, is the solution symmetric (shuffling around the box's length/width/height values doesn't change the answer), if you increase the height does the diagonal's length increase, if you scale all three sides does the diagonal scale the same amount, does it solve a related problem of the diagonal of a rectangle (box with height 0), are you using all the given data in the solution...) A point is that the math problem doesn't end with giving the answer, and similarly testing doesn't stop after you've verified the happy case or fulfilled some coverage requirement.

[0] https://github.com/ncredinburgh/QuickTheories/

[1] https://hypothesis.works/articles/intro/

[2] https://fsharpforfunandprofit.com/posts/property-based-testi...