(note: the following comment probably warrants a “rant” tag)

I have two alternative hypothesis for the explanation of the status quo.

First hypothesis is that state of the art in academia doesn’t necessary correlate with what is actually useful in practice. Not claiming (yet) that that’s what is happening with stateful property based testing, but I have a good example from a different area — there’s a lot of literature in academia about dealing with errors during parsing, and all that literature was not helpful to me when I had to solve the problem. Although I have read a tonne of papers on the topic, none ultimately feed into the solution that worked.

My second hypothesis is that academia is geared at proving to other academics that a paper is worth a publication, but is pretty bad at actually explaining ideas in a way that allows incorporating them into software people use. This post is actually an example of this. I am pretty much the target audience — I regularly use property based testing for my hobby stuff, my work thing is basically an appendage to one giant randomized test of strict serializability, I wrote a property-based testing library, and I think I formulated a specific idea which, while not a theoretical advancement, I think moved state-of-the-art of practice a little bit further.

I very much want to learn about a property-based testing technique which I should be using instead of what I use currently. But it’s very hard to use the present post to do that!

It starts with a very long-winded historical aside, which, while interesting, doesn’t really help me to learn anything. And than there are is series of examples which just bog down in Haskell’s idiosyncrasies, and it’s very hard to extract the actual idea out of the implementation gunk. This reminds me another recent case when I needed to learn about Reed-Solomon coding. The wikipedia page read like a wall of thick graffiti to me. And then I read https://mazzo.li/posts/reed-solomon.html posted here on lobsters, and it said, basically:

A polynomial of degree N is uniquely identified by N+1 points on its graph. Evaluate polynomial at M>N+1 points, give each point to a separate person, and then any N+1 people can recover the original polynomial.

I see this being repeated over and over — there’s a vast chasm between the essential simplicity of an idea which can often fit in a Tweet, and fluff and rigor which wrap the idea inside an academically-adjacent piece of writing.

I’d love to read a Tweet-sized explanation of what is stateful property-based testing, and how is it better than doing the same thing “by hand”.

Coming back to the first hypothesis: I do, in fact, have a suspicion that academic state of the art of property based testing isn’t all that useful in practice. I make two claims:

• You get 70% of the benefits of property-based testing if you pass in a PRNG to your test function.
• You get 85% of the benefits, if the PRNG is finite (at some point, instead of giving you heads or tails, it says error_out_of_entropy).

As a specific example, here’s how you can write a property test with minimization for the ring buffer (repo):

#[test]
fn test_queue() {
  arbtest::arbtest(|rng| {
    let len_max = rng.int_in_range(0..=10)?;
    let mut queue = Queue::new(len_max);
    let mut queue_model: VecDeque<i32> = VecDeque::new();

    while !rng.is_empty() {
      match *rng.choose(&["add", "remove"])? {
        "add" if queue_model.len() < len_max => {
          let x: i32 = rng.arbitrary()?;
          queue_model.push_back(x);
          queue.push(x);
        }
        "remove" if queue_model.len() > 0 => {
          let x_model = queue_model.pop_front().unwrap();
          let x = queue.pop();
          assert_eq!(x_model, x);
        }
        "add" | "remove" => (),
        _ => unreachable!(),
      }
      assert_eq!(queue.len(), queue_model.len())
    }
    Ok(())
  });
}

Minimization there is very simplistic, but it works well enough for this case. And you don’t need a tree of types&monads to use the thing, the rng is the familiar API of a random number generator.

In this sense, property based-testing reminds me the cottage industry of parser-combinator libraries: the idea lends itself very well to functional programming & static typing, but, in practice, production code tends to use a hand-written parser, because you can express all the same ideas in stupid first-order programming just fine. Same here — just pass in the rng!

Just today saw a recent talk from Python North Bay 2024 above improvements to hypothesis

Hypothesis Levels Up: codegen, observability, fault localization, and a black-magic backend

https://youtu.be/NRtAEXqo0rc?si=kqF1HD_Z14Qcrxqg

I hadn’t heard of “stateful” proptesting. Can someone tell me if I’m wrong on this? The way I’ve solved this is by just taking in a Vec<Action> and applying them where Action might be:

enum Action {Push(generated), Pop}

This has satisfied my needs historically. Where I’m imagining that this is insufficient is something where random sequences of Action aren’t valid? Like, I need some sort of rule that says “if the last generated was even the next one must be odd”? Historically if I’ve had these sorts of constraints I post-process the values but I can see how it may be desirable and more efficient for the framework to handle that, since the post-process means that the generated inputs aren’t what you actually test against.

edit: I misunderstood parallel testing - it’s for detecting races, not for performance.

My guess as to why these things aren’t adopted is simply because they aren’t that important. I love property tests and I use them plenty. When I’ve run into more complex property tests I haven’t found the frameworks to be overly limiting to me in the majority of cases. Given that in 90% of cases I’m totally happy, in 9% of cases I’m able to work around things, and perhaps in 1% of cases I just don’t write a proptest because it seems too painful, I don’t really think I would be motivated to do things differently and the work to meet those metrics is far less than the work to eat the last 10%.

This is an interesting writeup, but the title feels like taking two concepts and declaring them to be the most important things you can have in a property testing library, to the exclusion of all else, and I don’t think that’s obviously true.

On another point, it’s possible you should add jqwik may be worth considering for Java? It’s more actively developed than QuickTheories. I plan to consider porting my uses of QuickTheories to it, but that’s something I keep putting off.

This is a fascinating perspective to me because, while I know of QuickCheck and have used Haskell, I primarily use something like Hypothesis instead. And, if it’s not available in my language of choice, then Hypothesis provides a pattern which can be ported, even to dynamically-typed systems. This means that the closed-source claims don’t quite land for me; if Hypothesis were closed-source, I’d just write my own.

I liked the worked examples in the second half. It’s always fun to see what kinds of properties we can invent.

You may be interested in this 2016 list of QuickCheck alternatives from the author of Hypothesis, which is also the article from which that big list in Wikipedia is sourced.