Hello everyone! After more than 4 years of WIP development, I’m very excited to announce PropCheck.jl, a property based testing framework loosely inspired by QuickCheck & Hedgehog. It features type based generation, composition of generators,
filter of generated instances and automatic test-case shrinking/minimization. There are quite a lot of planned features, so please do check out the documentation! Some of these are quite a bit harder to do than others, so please be patient with me Contributions are always welcome though - I hope the internals are clear enough, though some parts definitely need more devdocs
A very early version of this package was used in the past to find an
unreachable reached catastrophic failure in Julia itself!
Due to the time already spent on developing this package, the currently latest version is 0.9.2, supporting Julia versions 1.6 and newer.
In a nutshell, property based testing means thinking about the (mathematical) properties you as a developer would like your code to have, and then testing/checking in some way whether these properties hold. This needn’t be exhaustive - just for
+(::Int64, Int64) there are already
2^128 possible input bitpatterns, too many to practically check completely. In a sense, property based testing as employed by PropCheck.jl is a form of fuzzing.
Aren’t unit tests sufficient? Well… No! If you can’t be sure that your code obeys the properties you would like it to have, you can get disastrously wrong results. In the worst case, you can end up drawing wrong conclusions from your scientific models, or crash your server in production due to a faulty assumption.
Not knowing about the desired properties & testing for them can lead to things like this - quoting Hillel Wayne (who specializes in formal methods):
In 2010 Carmen Reinhart and Kenneth Rogoff published Growth in a Time of Debt. It’s arguably one of the most influential economics papers of the decade, convincing the IMF to push austerity measures in the European debt crisis. It was a very, very big deal.
In 2013 they shared their code with another team, who quickly found a bug. Once corrected, the results disappeared.
Greece took on austerity because of a software bug. That’s pretty fucked up.
(This quote is from his article How do we trust science code?)
For a basic introduction to property based testing and how it relates to Julia in particular, please check out this section in the docs!
While efforts regarding formal specifications & machine checkable proofs are comendable, I think we can get quite far with property based testing & fuzzing before we need to tackle the dragon that is formal methods & verification. PropCheck.jl is decidedly not in the formal verification camp - it’s not an interface to SAT or SMT solvers, but a fuzzer. Said differently, property based testing + fuzzing are a fuzzy, statistical subset of full formal verification. You can think of running fuzzing tests as increasing confidence in the correctness of your code each time you run your testsuite, due to different inputs being chosen.
That being said, if this package becomes obsolete due to tremendous advances in formal methods & verification in Julia, I’ll happily retire this package to the annals of history
There are a number of other codebases related to property based testing (for example, JCheck.jl, QuickCheck.jl or RandomizedPropertyTest.jl) but to my eyes, they are either very old (10+ years!) and don’t support modern Julia, don’t support shrinking or don’t really compose their generators well, due to being based on QuickCheck. PropCheck.jl, while certainly taking inspiration from QuickCheck, is using a mixed approach, focusing on integrated shrinking. This has advantages and disadvantages, but from my experience with the package so far, the current architecture is pretty extensible and works much better than a plain implementation of QuickCheck (Julia is much less focused on types than Haskell is, after all; much of the information we have about a type is implicit & not guaranteed, and even with that, some type based shrinks are just plain bad, due to even their types not capturing the full semantics of the produced values). Most of the features currently in PropCheck.jl came about because I ran into an issue that I wanted to solve when testing a different codebase - hence, the package is already at 0.9.1
One issue with developing a package in private for such a long time is that it can happen that I’m missing an obvious use/fatal error case that I just didn’t think about/haven’t encountered due to knowing the “happy path” of the package, so to speak - so please do give the package a try and report errors, bugs & feature requests at the issue tracker!
Finally, I’d like to thank the fine folks at the JuliaLang Zulip, in particular @Mason, @jakobnissen, jar and Michael Fiano (not sure about the discourse names, sorry!) for giving the first draft of the documentation a good look-over and spotting some issues