I know it’s not the same thing, but PBT’s can catch all sorts of absolutely crazy bugs that I never would think to check for. Stateful stuff, cross-service stuff. My only gripe with PBTs has always been the tedious setup, but LLMs solve that.
I haven’t seen much discussion around PBTs lately, but you get a ton of bang for your buck in the LLM age
What's funny though is that the reasoning needed to say some sampling is comprehensive....makes it closer fo proofs! AFL — coverage-based fuzzing — was the original innovator here, but imagine an interpreter — code coverage in the interpreter itself isn't so good, you also want to explore the interpreted program!
This is why "is my testing comprehensive?" is actually an open-ended problem that, in the limit, is just as hard as formal verification.
I suspect we're basically going to see a convergence here. Randomized testing can be called "Monte Carlo formal verification" hehe.
Well said! I learned about PBT in the first place because I watched a talk where the speaker referenced the story of foundationDB. Super interesting stuff. If anybody wants a link I can dig it up
But they are very different IMO at what they focus on and so they occupy different places when talking about does a piece of software does what it should do and withing the state/parameters specified:
- Property based testing focuses on finding counter examples - Formal verification focuses to prove that a property always holds
More than this I think in all these discussions we are missing the most important piece: validation.
While verification means to prove or test or verify that the software does what is should do, validation means to prove or test or verify that the software is solving user needs.
I still found it useful for
1. trusting a bit of code is correct
2. rule-dense bits of code (eg something like a date parser)
The real issue so far is that I'm having trouble finding tasks where an LLM can't correctly code up an exhaustively defined spec.