The sad state of property-based testing libraries
stevana.github.io
stevana.github.io
https://www.tedinski.com/2018/12/11/fuzzing-and-property-tes...
Like, with the below fuzz test, and the corresponding invariant checks, isn't this all but equivalent to property tests?
https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
But I'd take one step back, and ask a more meta question about testing: does a successful test mean successful code, and vice-versa? Is there anything in Go's contract that specifies that the same inputs to the same code will yield the same output?
A successful test implies that the documentation is true. That is, after all, why you are writing tests: Documentation – To explain to future developers the intent and usage behind the code you wrote. You could just as well write the documentation in Word instead, but then you'd lose the ability to perform machine verification of the documentation, which is a huge boon to moving codebases where the documentation and code are likely to fall out of sync if one is not incredibly careful (although perhaps LLMs will some day bridge that gap?).
The documentation being true does not imply that the documentation is useful, of course. Writing useful documentation is still an art.
A few jobs ago I would often be in a team where the entire team had turned over several times, we would be asked to do large updates to a legacy application or bump lots of dependencies and just not break anything. When pushed the product owner wouldn’t be able to describe what the app was supposed to do, particularly for unusual types of users (the account / user modelling was chaotic so say, several billing accounts per user, each with different products and access levels). At that point “foo calls bar” doesn’t clarify much intent.
I find when I do this I don’t need to write by hand anywhere near as many tests to get my software working well. I also usually turn any failures found by the fuzzer into standalone unit tests, to make any regressions easier to find later.
I coded some tests that ensure the data structure is useful, many of them test examples from papers describing the data structure, but that don't necessarily cover all the corner cases.
Then I fuzzed it. I used Go's fuzzer, which is geared towards parsers and stuff. It can generate a stream of bytes and use that for fuzzing. The data structure is a set/map. So I interpret the stream of bytes as commands to add/remove random elements from the set/map. After I add an element, contains needs to return true; after I remove one, contains need to return false; if I put in a mapping, finding it must return what I just put there, etc. And at every step all the data structure invariants (that ensure logarithmic search, etc) need to hold.
That was stupidly effective at finding a few bugs, all within seconds, all with sequences of less than a dozen operations. Then it stops. And you get 100% coverage.
I'm assuming that, apart from ergonomics, where I kinda build my own state machine transitions out of a stream of bytes, the tooling actually seems more effective than property testing libraries.
Still curious to understand what I'm missing out.
However, depending on the lib, you can get some nice quality of life improvements. One "nice to have" is shrinking. See the "Shrinking" section here https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
Having combinators to compose generators is also great.
Libs may also have a known set of "bad" values that cause exceptional behavior.
Not sure how effective it is compared to other options, but I'm not totally missing out there.
It also builds a corpus of interesting inputs over time (those that cause new branches to be taken, since that's its goal: improve coverage).
I'm less sure about combinators.
Traditional property based testing is implemented simply as a library, so they don't necessarily have coverage information to guide their random input generation.
- Quick running tests, detailed assertions —> PBT
- Longer tests, just looking for a crash —> fuzzing.
- In between, who knows?
https://hypothesis.works/articles/what-is-property-based-tes...
Under this point of view, a property-based testing library is really two parts:
1. A fuzzer.
2. A library of tools for making it easy to construct property-based tests using that fuzzer.
My current strategy is to interpret a byte stream as a sequence of "commands", let those be transitions that drive my "state machine", then test all invariants I can think of at every step.
What's the intent behind building on top of Go's fuzzer as opposed to an approach like testing/quick takes?
Also: https://news.ycombinator.com/item?id=30385195
But, it occurs to me I could try and build on the same API, and compare them for effectiveness.
Indeed. And respect to software that knows when it is complete, but is there some relevance to this here?
> Also: https://news.ycombinator.com/item?id=30385195
While the distinction between fuzzing and PBT is, er, fuzzy, what is unquestionable is that PBT is not meant to be coverage driven. It is a means to document behaviour for other developers in a way that is, in some cases, more descriptive than providing a fixed set of examples or other "traditional" ways of providing such documentation. Seeking coverage and "interesting" cases, rather than providing documentation, is decidedly the role of fuzzing.
What you describe (commands) is commonly used with model based testing and distributed systems.
> Python is Turing complete, but does [TLA,] need to be? Is there an in-Python syntax that can be expanded in place by tooling for pretty diffs; How much overlap between existing runtime check DbC decorators and these modeling primitives and feature extraction transforms should there be? (In order to: minimize cognitive overload for human review; sufficiently describe the domains, ranges, complexity costs, inconstant timings, and the necessary and also the possible outcomes given concurrency,)
From "S2n-TLS – A C99 implementation of the TLS/SSL protocol" https://news.ycombinator.com/item?id=38510025 :
> But formal methods (and TLA+ for distributed computation) don't eliminate side channels. [in CPUs e.g. with branch prediction, GPUs, TPUs/NPUs, Hypervisors, OS schedulers, IPC,]
Still though, coverage-based fuzzing;
From https://news.ycombinator.com/item?id=30786239 :
> OSS-Fuzz runs CloudFuzz[Lite?] for many open source repos and feeds OSV OpenSSF Vulnerability Format: https://github.com/google/osv#current-data-sources
From "Automated Unit Test Improvement using Large Language Models at Meta" https://news.ycombinator.com/item?id=39416628 :
> "Fuzz target generation using LLMs" (2023), OSSF//fuzz-introspector*
> gh topic: https://github.com/topics/coverage-guided-fuzzing
The Fuzzing computational task is similar to the Genetic Algorithm computational task, in that both explore combinatorial Hilbert spaces of potentially infinite degree and thus there is need for parallelism and thus there is need for partitioning for distributed computation. (But there is no computational oracle to predict that any particular sequence of combinations of inputs under test will deterministically halt on any of the distributed workers, so second-order methods like gradient descent help to skip over apparently desolate territory when the error hasn't changed in awhile)
The Fuzzing computational task: partition the set of all combinations of inputs for distributed execution with execute-once or consensus to resolve redundant results.
DbC Design-By-Contract patterns include Preconditions and Postconditions (which include tests of Invariance)
We test Preconditions to exclude Inputs that do not meet the specified Ranges, and we verify the Ranges of Outputs in Postconditions.
We test Invariance to verify that there haven't been side-effects in other scopes; that variables and their attributes haven't changed after the function - the Command - returns.
DbC: https://en.wikipedia.org/wiki/Design_by_contract :
> Design by contract has its roots in work on formal verification, formal specification and Hoare logic.
TLA+ > Language: https://en.wikipedia.org/wiki/TLA%2B#Language
Formal verification: https://en.wikipedia.org/wiki/Formal_verification
From https://news.ycombinator.com/item?id=38138319 :
> Property testing: https://en.wikipedia.org/wiki/Property_testing
> awesome-python-testing#property-based-testing: https://github.com/cleder/awesome-python-testing#property-ba...
> Fuzzing: https://en.wikipedia.org/wiki/Fuzzing
Software testing > Categorization > [..., Property testing, Metamorphic testing] https://en.wikipedia.org/wiki/Software_testing#Categorizatio...
--
From https://news.ycombinator.com/item?id=28494885#28513982 :
> https://github.com/dafny-lang/dafny #read-more
> Dafny Cheat Sheet: https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZ...
> Looks like there's a Haskell-to-Dafny converter.
haskell2dafny: https://gitlab.doc.ic.ac.uk/dcw/haskell-subset-to-dafny-tran...
--
Controlled randomness: tests of randomness, random uniform not random norm, rngd, tests of randomness:
From https://news.ycombinator.com/item?id=40630177 :
> google/paranoid_crypto.lib.randomness_tests: https://github.com/google/paranoid_crypto/tree/main/paranoid... docs: https://github.com/google/paranoid_crypto/blob/main/docs/ran...
I still think the usual combinators (map, filter, chain, and oneOf, to use fast-check’s names) can be a bit awkward, so I’m writing a new property testing library for JavaScript that hopefully works a bit nicer. (Experimental and not published yet.)
For example, let's say our test data is an assoc-list like `[(Int, Customer)]`, and there's a bug that's triggered by repeated keys. LazySmallcheck will run the test on the most general assoc-list there is, a _|_ value!
myTest (exception A) --> throws A
myTest [] --> test passes
myTest (exception A:exception B) --> throws A
myTest ((exception A, exception C):exception B) --> throws A
myTest ((0, exception C):exception B) --> throws B
myTest ((0, exception C):[]) --> passes
myTest ((0, exception C):exception A:exception B) --> throws A
LSC hence won't try specialising `exception C`; but it will try "larger" Int values, e.g. `(1, exception C):[]`, `(-1, exception C):[]`, etc. up to a pre-defined "depth". I'll ignore these cases and focus on the branch with the longer list:
myTest ((0, exception C):(exception A, exception D):exception B --> throws A
myTest ((0, exception C):(0, exception D):exception B) --> FAIL!
That's more informative for understanding this bug than e.g. Smallcheck or QuickCheck, whose "minimal" counterexamples would be fully-specified values, like `(0, Customer { name = "", orders = [], discount = Nothing, joined = 1970-01-01 }):(0, Customer { name = "", orders = [], discount = Nothing, joined = 1970-01-01 }):[]`.
Hence LSC's approach has three interesting features:
- It has a coverage-like approach that homes-in on interesting cases, by gradually generating the parts of a value that get forced (which are usually the parts being branched on)
- It can indicate which parts of a counterexample are irrelevant for the failure
- It can prove some properties universally (i.e. when that input is irrelevant to the pass result)
It seems like Hypothesis is unable to handle simple but "large" data sets >>by design<<, where "large" is really not so large. [0] It was such a pain that we ripped out Hypothesis (and generative testing altogether, sadly) completely from our python test suite at work.
[0] https://github.com/HypothesisWorks/hypothesis/issues/3493
someone in that thread suggested that you use a different instance generation strategy that can't generate zeroes, instead of rejecting the instances hypothesis's shrinker most loves to generate, once they are generated. did you try that?
how does clojure.spec.alpha handle this differently?
in mjaniczek's comment at https://news.ycombinator.com/item?id=40876437, they call out your case as a disadvantage of hypothesis's approach:
> The disadvantage is that the generators are now parsers from the lists of bytes that can fail (introducing some inefficiency) and user can make a crazy generator that the internal shrinker will not be able to shrink perfectly. Nevertheless, it's the best DX of the three approaches, ...
though presumably you wouldn't agree that your test was written in a 'crazy' way
this should read "hypothesis was unable". we regret the error. those responsible have been sacked
There’s usually always a point where further shrinking is not possible.
you make it sound like clojure.spec.alpha doesn't do shrinking at all. possibly you don't know what shrinking is? shrinking keeps your results from looking "random" by simplifying them until all the simpler versions of the test case pass, so it finds the simplest failing case instead of a "random" one. this also enables hypothesis to be a lot more aggressive at looking for failing cases, for example by generating much larger test data sets than you would want to pore over, because if it finds one that fails, it will shrink it before showing it to you
if i've misunderstood you and clojure.spec.alpha does do shrinking, what does it do in the case where your test case is written to reject all but an exponentially small fraction of shrunk cases? does it just take an exponentially long time to run your test suite? is that what you mean by 'just works'?
If you generate stuff randomly, then filter out stuff matching some property, you're basically playing the lottery while generating!
In any case, even in the case you describe, I would not expect the strategy to fail with probability 1. Remember that this generates multiple samples, and only one of these need to be valid.
This page lists the artifact evaluation criteria for a handful of conferences:
Maybe that's already being done though!
FWIW, my own opinion on that political question is that current standards are way to loose. After all, nobody is forced to publish anything. There is a lot of research happening in the world, that is never published anywhere (e.g. because of proprietary value). It will never go away (unless the world reaches some communist-utopia, but even then it will be doubtful for other reasons). But if one works in academia (and, God forbid, receives grants for his work!) and his stated goal is to move world's scientific knowledge further, it's only fair to ask for him to actually follow that goal, and not just simply pretend following that goal in order to move up that twisted ladder of his academic career.
Having more requirements towards that end is unlikely to impact the number of papers published.
The more severe problem with published papers is mistakes often deliberately overlooked in order to publish as much and as fast as possible. Having papers being easier to verify has a chance of improving this situation... but I wouldn't hold my breath. People are very good at cutting corners.
For parallel testing I guess it can be useful at times, but often it's easier to just run a bunch of tests in parallel instead.
let mut rng = rand::thread_rng();
for action_count in 1..4 {
for _ in 0..10_000 {
let seed = rng.gen::<u64>();
eprintln!("let seed = {seed};");
let mut rng = ChaChaRng::seed_from_u64(seed);
then generate a seed to seed a deterministic PRNG, and print it out so if the test fails, I just copy and paste the error seed to replay the error case
I have found doing this manual proptesting to be faster, more flexible, and generally less fuss than using any frameworks or libraries
That said, for really robust concurrency testing, I cannot recommend enough the AWS Shuttle library (https://github.com/awslabs/shuttle) which can find insanely complicated race conditions. I wrote a little tutorial on it here: https://grantslatton.com/shuttle
We used it at AWS to verify the custom filesystem we wrote to power AWS S3.
For example, say I’m testing a data structure. I’ll have an outer loop that picks a seed and an inner loop that does ~100 mutations of a data structure instance, testing assertions each time. If there’s a failure, I’ll try a bunch of seeds to look for one that fails the fastest. (In the fewest possible inner loop iterations).
It’s not a perfect system, but for most bugs I can usually get a test case that only needs 5-10 steps before a crash occurs. And if the reduction step finds a different bug? That’s no problem at all. I fix what I found and go back to trying more seeds.
What I miss is: Shrinking, deterministic replay.
type Instruction = | Read of stuff | Write of stuff | Seek of stuff | …
And then the property is "given this list of instructions, blah". The `StateModel` formalism requires doing basically the same work! I really don't see that `StateModel` is pulling its weight: it's adding a bunch more framework code to understand, and the benefit is that it's getting rid of what is in my experience a very small amount of test code.
That would be the benefit.
In the case of .NET, there is https://github.com/microsoft/coyote which works by rewriting IL to inject hooks that control concurrent execution state.
It would have been much more expensive to have a custom interpreter specifically for this task (CoreCLR never interprets IL).
This approach somewhat reminds me of precise release-mode debugging and tracing framework for C++ a friend of mine was talking about, which relies on either manually adding the hooks to source files or doing so automatically with a tool.
That is, if the issue persists. There's one that mentions F# submitted in 2020, but nothing else since: https://github.com/microsoft/coyote/issues/39
Edit: Whoops, meant to reference this one: https://stackoverflow.com/questions/61694051/how-to-use-micr...
I don't understand why there is less tolerance for having to make accommodations or take extra steps when working with F# than, let's say, when using Kotlin or Scala. Both follow a similar pattern where they can use pretty much every Java library by virtue of targeting JVM but can't use a huge amount of Java-only tooling that does meta-programming or instrumentation beyond what is provided by JVM bytecode specification, and yet it's not seen as such a huge ordeal from my surface impressions.
In general the F# way is to write completely different stuff, right, either hiding away the underlying C# or completely replacing it. Witness the existence of the SAFE stack, Giraffe to hide the egregious ASP.NET, the totally different approaches with statically resolved type parameters in F# vs enormous hierarchies of interface types in C#, Myriad AST generation vs Roslyn stamping out strings, etc. I have no opinion on the languages hosted on the JVM, but there is a really nontrivial impedence mismatch between idiomatic C# and F#!
If any operation is valid in any state and you just want a totally random sequence of arbitrary operations, then yeah a stateful proptest framework may be overkill. But if you need to maintain a model state and specify preconditions for different operations, having a dedicated framework saves a lot of work.
I wrote a blog post about this stuff last year, if you’re interested in some more in-depth examples: https://readyset.io/blog/stateful-property-testing-in-rust
Also, as others have mentioned, parallel state machine testing is another really cool benefit you can get from having a dedicated framework, but it’s not the only benefit.
One of these is coverage guided PBT, check eg. Dan Luu's article: https://danluu.com/testing/
Another one, which I'm biased towards, is making shrinking automatic while keeping all the invariants you created while generating the values. I have a talk on this but the TL;DR is that
- derived QuickCheck-like shrinker functions that work on values (shrink : a -> [a]) have issues with the constraints, making people turn off shrinking instead of dealing with the issues
- rose tree "integrated shrinking" (eg. Hedgehog) follows the constraints of the generators, but has issues with monadic bind (using results of generators to dispatch to another generator)
- the only approach that seems to magically "just work" is Hypothesis' "internal shrinking", which uses a layer of indirection to shrink lists of random choices instead of the values themselves. The disadvantage is that the generators are now parsers from the lists of bytes that can fail (introducing some inefficiency) and user can make a crazy generator that the internal shrinker will not be able to shrink perfectly. Nevertheless, it's the best DX of the three approaches, and given it's a small miracle people are testing at all, feels to me like the approach most worth building on as a testing library author.
We're at the limits of my amateur knowledge, but I believe this is a fundamental limitation of monadic bind/generators. Instead, you should prefer applicative generators for optimal shrinking. https://github.com/hedgehogqa/haskell-hedgehog/issues/473#is...
In other words, applicative generators do not use "results of generators to dispatch to another generator", but instead shrinking is optimal due to the "parallel" nature of applicatives (I'm using "parallel" in the monadic sense, and not the sense of article's "threading" sense). Since applicatives are "parallel", they can shrink the generators independently. (Whereas monadic generators are in "series" and therefore shrinking one necessarily changes the behavior of the subsequent generator, as you noted.)
Please feel free to link your talk if it's public!
But always interesting to discover an avenue I haven't explored before :)
You can think of `let!` as `let + await`, and `let! x ... and! y` as `await Parallel([x, y])`.
Please feel free to ask any questions if it's still confusing!
promise.then(...).then(...).then(...)...
To have an idea about applicatives being parallel, think about a list of functions, and a list of values; each function would be applied to a corresponding value, resulting in a list of results:
results = []
for ix in range(functions):
f = functions[ix]
x = values[ix]
results.append(f(x))
(Why would one care about this all? Because many daily things are functors, applicatives, and monads, e.g. a list is usually all three.)
[Disclaimer: I don’t know how QuickCheck actually works, so I’d appreciate a sanity check (hah) of the following from somebody with actual knowledge on the matter.]
GP’s point, if I understood it correctly, is as follows. If you’re doing randomized testing, then g and h could perhaps be defined as { for (i=0; i<n; i++) { int x = rand(); if (!fork()) return x; } } (and yes, in monad-land the moral equivalent of fork() is admissible as what I vaguely called a “stateful computation”). You see how strict ordering of side effects enforced by monads essentially forces you into a depth-first search of the state space (although I guess you could do iterative deepening?), while applicatives can allow for different exploration strategies (ones more interesting than C’s official behaviour of “that’s UB, you fool”).
Dependency-driven de facto evaluation orders have always existed in C though: things that you can figure out must be ordered even though there isn't a sequence point.
The standard spells out that expressions like i = i + i are okay, but actually it's not necessary to do so. The assignment cannot take place until the assigned value is known. The assigned value is not known until the + is evaluated and the + cannot be evaluated until the operand values are retrieved. Therefore, the retrieval of the prior value of i necessarily precedes the movement of the new value into i.
This, rather than sequence points, is rather a bit like monadic sequencing.
Of course it can. It's retrieving the value out of the lvalue is what cannot be done and even then you can still stretch this delay further with the "as-if" rule. Haskell does something similar with its lazy evaluation IIRC.
That’s exactly my point. Writing g >>= \x -> h >>= \y -> f x y is like writing (x = g(), y = h(), f(x,y)), with an arbitrary ordering between computations g and h that the programmer is forced to choose, whereas f <$> g <*> h is like f(g(), h()), with no ordering between g and h imposed by the applicative model itself, similar to the absence of a sequence point between sibling arguments in C.
Contrast with a test data generator that randomly chooses the first field, and then calculates the second field based on the first field’s value. The framework can’t directly mutate the second field because there’s a data dependency. If it just changes the second field, it will get a record that couldn’t have been generated.
The Hypothesis test framework took a different approach. Instead of mutating the test data directly, it mutates the “random” input and reruns the generator. If you do shrinking that way, you always get valid test data, though it might not be very similar to the original.
This is similar to what fuzzers do - you start with unstructured binary data and build data structures out of it. Your “random” test data generator is really a parser of random (or maybe not so random) input.
I agree using applicatives helps somewhat, it basically minimizes your usage of bind.
Hypothesis works around this (and gets a bind that shrinks nicely) by recording those choices into (in principle) a flat list, and shrinking that. So your shrinker can work on both "before the bound fn" and "after it" at the same time, but the result might be something that the generator can't parse back into a value.
I did have quite a bit of prior experience with clojure.spec.alpha (with or without test.check), so despite some differences it's not like I was completely alien to the general ideas.
[0] https://github.com/HypothesisWorks/hypothesis/issues/3493
So if that is intentional and by design, then you’re right, I don’t understand.
That's actually one big reason I prefer Hypothesis over eg Rust's proptest, which makes no attempt to give you 'nasty' numbers. Last time I checked, QuickCheck didn't make any attempts to give you floats well-known to cause trouble either (like inf, negative inf, different NANs, 0, 1, -1, the least positive float, the largest negative float, the largest finite float just before infinity etc.)
Anecdotally, I have triggered many more bugs with the edge-case-preferring generation:
Basically, that was me using Rust's proptest library which does uniform generation by default, and I hacked it up to prefer edge cases. For simplicity, for eg u32 I set it up to with something like 50% probability to pick one from 0, 1, 0xFFFF_FFFF, 2, and a few other special values, or to pick uniformly at random.
I vaguely remember some research that compared carefully hand-picked values vs property based testing. And the carefully hand-picked values performed slightly better at the same number of test cases. But if you modesty increased the number of test cases generated for property based testing, that swamped the advantage of careful hand picking.
Similarly, I suspect that any disadvantage that might exist for the scheme I outlined above compared to uniform sampling would go away, if you increased the number of test cases slightly. At least as long as you give a decent chunk of probability weight in my scheme to uniform sampling.
This is totally understood and expected. But a “probability distribution” of exactly ONE value with P=1 is not much of a distribution.
I don’t understand this response, because it doesn’t address the issue at all.
It was able to generate values just fine ([1]), so your problems might have been just some issue of the Hypothesis _implementation_ instead of something wrong with the general algorithm?
Note that your usage of Hypothesis was "weird" in two aspects:
1. You're using the test runner for generation of data. That's sometimes useful, particularly when you need to find a specific example passing some specific non-trivial property (eg. how people solve the wolf, goat, cabbage puzzle with PBT - "computer, I'm declaring it's impossible to solve the puzzle, prove me wrong!"), but your particular example had just "assert True" inside, so you were just generating data.
There might be libraries better suited to the task. Elm has packages elm/random (for generation of data) and elm-explorations/test (for PBT and testing in general). Maybe Clojure or Python have a faker library that doesn't concern itself with shrinking, which would be a better tool for your task. The below gist [1] has an example of using a generator library instead of a testing library as well.
2. You were generating then filtering (for "at least one non-0 values across a column"). That's usually worse than constructively generating the data you want. An example alternative to the filtering approach might be to generate data, and then if a column has all zeroes, generate a number from range 1..MAXINT to replace the first row's column with. Anyways, "all zeroes" shouldn't happen all that often so it's probably not a huge concern that you filtered.
[1]: https://gist.github.com/Janiczek/c71050aa89fb0b19d73e683f9a3...
> Anyways, "all zeroes" shouldn't happen all that often so it's probably not a huge concern that you filtered.
This is really the point.
Like I said, Clojure’s spec (with or without test.check) has no trouble.
> - the only approach that seems to magically "just work" is Hypothesis' "internal shrinking", which uses a layer of indirection to shrink lists of random choices instead of the values themselves.
My preferred framework is falsify, which provides "internal integrated shrinking". It's similar to Hypothesis, but uses a tree of generators rather than a linear sequence (it's based on "selective functors", which are a nice interface that's also useful for e.g. validators).
From https://hackage.haskell.org/package/falsify
> This library provides property based testing with support for internal integrated shrinking: integrated in the sense of Hedgehog, meaning that there is no need to write a separate shrinker and generator; and internal in the sense of Hypothesis, meaning that this works well even across monadic bind.
For example, a lot of times I might have two implementations, a naive one that's slow and simple, and an optimized one. I can compare the output of both against each other on arbitrary input. That's a simple property that easy to understand, but hard to put in the type system in general.
Similarly, I often have properties that eg the order that input is presented in shouldn't matter, or sometimes you have ways to partition your data 'max(maximum over A, maximum over B)) = maximum(A union B)'. How do you encode that in the type system?
Or you have something like 'for any A and B: (find some optimal solution over A) is worse than (find some optimal solution over (A union B))'. Or you have idempotency like 'f(f(A)) = f(A)'.
These are all easy to understand properties, but not trivial to describe in most type systems.
Parallel testing is interesting, but hasn't been a large source of pain yet.
See: - https://github.com/AnthonyLloyd/CsCheck?tab=readme-ov-file#m... - https://github.com/AnthonyLloyd/CsCheck?tab=readme-ov-file#c...
Besides, it would be really cool to have property-based integration or hybrid unit/integration tests. Or even property-based E2E tests. Unfortunately, the setup of the example will almost always take too long for a relevant set of runs.
For instance: If you have a basic data model (say in sqlalchemy) and want to write property-based tests (say in hypothesis), you can relatively quickly derive strategies for the models (but beware of recursion and primary keys). But writing that model instance into the DB for running an example just takes too long for swift testing.
Big fan of property testing.
A particularly big fan of Hedgehog.
I tried writing a Hedgehog-inspired library in Rust and realized how complex the underlying domain is.
For example, the RNG is "splittable" [1][2] which means you can take a deterministic seed and split it in two, e.g. for parallel generators to work independently but still deterministically. The effort that has gone into this feature level is a little numbing. I have an awe similar to that of the "fast inverse square root" hack when I see code like this:
-- | A predefined gamma value's needed for initializing the "root" instances of
-- 'Seed'. That is, instances not produced by splitting an already existing
-- instance.
--
-- We choose: the odd integer closest to @2^64/φ@, where @φ = (1 + √5)/2@ is
-- the golden ratio.
--
goldenGamma :: Word64
goldenGamma =
0x9e3779b97f4a7c15
[1]: https://hackage.haskell.org/package/hedgehog-1.4/docs/src/He...
[2]: https://gee.cs.oswego.edu/dl/papers/oopsla14.pdf
[3]: https://github.com/hedgehogqa/haskell-hedgehog/issues/191
Wonder why most property-testing libaries don't have features like this?
The libraries require training to use. And they're not that easy to write.
> the current state-of-the-art when it comes to property-based testing is stateful testing via a state machine model and reusing the same sequential state machine model combined with linearisability to achieve parallel testing
Okay, okay. I admit I've never performed property-based stateful testing, nor in parallel. So that may be the coolest feature out there, because it addresses one of the hardest problems in testing.
But I think that yet other things have happened with modern property-testing libraries (e.g. Hypothesis, PropEr, Hedgehog, Validity):
Shrinking for free [4], generators for free [5], defining the probability distribution of your sub-generators in a composable way.
Maybe those features are not as significant, but they're equally missing from almost all property-test libaries.
[4]: Gens N’ Roses: Appetite for Reduction • Jacob Stanley • YOW! 2017 https://www.youtube.com/watch?v=LfD0DHqpeVQ
[5]: https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
Eg try java’s random prng library, and generate a few booleans with two seeds very close to each other.
Then try apache common’s merseine twister prng.
You could try to somehow be clever about how you generate the inputs: ("A" + nonempty string | "B-Z" ++ possibly empty string)
Or you could generate a string, check it for "A"-ness, and if true, fix it before running the actual test by appending some random non-empty string after it.
The three approaches might look like (in pseudocode)
1. Filtering
gen.string().filter(s => s !== "A")
2. "Smart" construction
gen.oneOf([ "A" + gen.string().nonempty(), gen.charBetween("B","Z") + gen.string() ])
3. Naive generation + fix
gen.string().andThen(s => (s === "A") ? s + gen.string().nonempty() : s)
If you ask for an integer but only want odds (as an example), 50% of the generated values will be tossed out with filtering. If you instead take every integer and make them odd (double and add 1, for instance) then all the generated inputs will be usable.
One pitfall with non-coverage-driven randomized testing like QuickCheck, is that how good your tests are depends a lot on the generator. It may be very rarely generating interesting inputs because you biased the generator in the wrong way, and depending on how you do the generation, you need to be careful to ensure the generator halts. With coverage-driven fuzzing all of these problems go away; you don’t have to be smart to choose distributions so that interesting cases are more common, coverage instrumentation will automatically discover new paths in your program and drill down on them.
But isn’t fuzzing about feeding a large program or function random bytestrings as inputs, whereas property-based testing is about testing properties about data structures? It is true that fuzzers operate on bytestrings, but there is no rule that says we can’t use that bytestring to generate a data structure (in a sense, replacing the role of the random seed). And indeed this is what the Arbitrary crate [1] in Rust does, it gives tools and even derive macros to automatically generate values of your data types in the same way that QuickCheck can. The fuzzing community calls this Structure-Aware Fuzzing and there is a chapter about it in the Rust fuzzing book [2]. There are also tools like libprotobuf-mutator [3] that substitute fuzzers’ naive mutation strategies, but even with naive strategies fuzzers can usually get to 100% coverage with appropriate measures (e.g. recomputing checksums after mutation, if the data structure contains checksums).
I am using this extensively in my own projects. For example, RCL (a configuration language that is a superset of json) contains multiple fuzzers that test various properties [4], such as idempotency of the formatter. In the beginning it used the raw source files as inputs but I also added a more advanced generator that wastes less cycles on inputs that get rejected by the parser. The fuzzer has caught serveral bugs, and most of them would have had no hope of being found with naive randomized testing, because they required a cascade of unlikely events.
Structure-aware fuzzing is not limited to generating data structures either, you can use it to generate reified commands to test a stateful API, as you describe in the _Stateful property-based testing_ section. The Rust fuzzing book has an example of this [5], and I use this approach to fuzz a tree implementation in Noblit [6].
[1]: https://docs.rs/arbitrary/latest/arbitrary/ [2]: https://rust-fuzz.github.io/book/cargo-fuzz/structure-aware-... [3]: https://github.com/google/libprotobuf-mutator [4]: https://docs.ruuda.nl/rcl/testing/#fuzz-tests [5]: https://rust-fuzz.github.io/book/cargo-fuzz/structure-aware-... [6]: https://github.com/ruuda/noblit/blob/a0fd1342c4aa6e05f2b1c4e...
I implemented a stupid simple shrinker for arbitrary, and I’d love to know a specific example where it fails to shrink in a good way:
https://github.com/matklad/arbtest/blob/0191f93846e9f7e38254...
I know at lest two interesting approaches for making that way smarter, but I don’t yet have a problem where my dumb approach isn’t sufficient.
You can easily write a JS function that can have a race condition by launching two asynchronous processes (such as writing to local storage in a browser or the file system both operating on the same data).
I had this happen just today while scraping different websites writing to the same files and overwriting each other.
First off, the "training" problem is a very real and fundamental blocker. I think academics or less experienced engineers see it as a problem of education, but I believe it's actually an engineering/organizational problem: for a company or even OSS project, when you use niche/unadopted tools like this you either need to provide training for it or you massively shrink the set of people able to work on your project by requiring or expecting them to learn it on their own. This introduces a practical headache bigger than the ones a tool like this solves (since these are just incrementally better ways to test software) - you get less contributions or need to spend more on getting people onboarded. Note that even if "training" people is free in the sense that there is no paid training material, you still pay a cost in lower productivty for new people and the time spent training.
Even once people are trained, you now have a process/institutional need to support the property based tests you wrote. That may mean paying for licenses for software, or maintenance of whatever infrastructure/integrations you write to get property based testing working in your developer workflow. And you also now need to rely on people using these tools correctly - the problem with formal verification is that it doesn't verify that you're actually solving the real problem correctly, just that your program operates as expected (ie it only verifies that your software is Working As Implemented, not Working as Intended). The more you rely on average joes to wield complex things like this well, the more headaches you introduce - if the bottom 10% of people you hire use it sloppily or wrongly, once you're past a few dozen regular contributors you're basically going to have constant issues. You see this all the time with even just regular unit and integration tests - less capable developers constantly introduce flakes or write tests so bad/basic that it'd be better for them to not even be writing tests at all.
Even if after considering all that it still seems a worthy tradeoff, there's the question of whether property based testing solves the problem you think it does. As I mentioned, it can moreso verify software is Working as Implemented rather than Working as Intended. But there is the bigger problem of major software projects not conforming to the simpler use cases that sell people on using this tool. In my experience stateless functions almost never have bugs, and when they do, it's mostly a "requirements discovery" problem you wouldn't catch with any kind of verification tooling.
Stateful verification becomes a problem in the kinds of real systems programming projects like the Linux Kernel or Qemu which stand to benefit most from verification. If you're verifying things at the level of a "higher level" abstraction like a scheduler, you almost always have really high dimensionality/a lot of state, perhaps deceptively more than you think, because of composition. And you tend to also have a devloop that is already very slow - builds take a long time, and running tests of higher level components can be "expensive" because it may take 100ms-1s for something like a kernel to finish starting in a test environment. For a single test that's nothing, but multiplied across all tests makes testing painful enough already; adding 3x or 100x by doing property based testing with new tests, even if pruned before submitting, could be either hugely expensive or way too slow. And similarly, the increased resource requirements to maintain state machines can be very expensive. TSAN does essentially parallel property-based testing and introduces 128-512 bytes of overhead for every 8 bytes of memory under test: https://github.com/google/sanitizers/wiki/ThreadSanitizerAlg....
Is it cool and underrated? Definitely. But it's not a silver bullet and honestly just isn't worth it for most software. Even when it is worth it, it has its drawbacks.
Today a weird, scary splinter faction of the already terrifying Effective Altruism religion/cult is talking about building digital gods they can’t control and saying with a straight face that this is imminent (absurdly extravagant claim with no evidence more convincing than a logarithmic scale and a ruler) and using this as an argument to redefine everything from the definition of science to the very epistemology of factuality and getting the public to directly or indirectly subsidize it into the bargain.
People who make Ray Kurzweil’s Singularity magical thinking look flat fucking normal and frankly sound like L Ron Hubbard more every day are unilaterally deciding that all research into, ya know, what they claim is the most important event in human history is totally black box propriety because, ya know, for our own good.
I’ll take the polite Swiss functional programming folks over Anthropic’s Mechanical Interpretability people seven days a week and twice on Sunday.
Can we go back to this please? The new thing sucks.