I’m back from this year’s Bug Bash conference. I was a big fan of the first one. Did the sophomore effort live up to the energy and execution of last year? Or has AI automated away the correctness community, leaving us with nothing left to talk about? Tune in for the verdict.
The inaugural Bug Bash conference was really special. I’ve been to many conferences, but this was legitimately the first that I felt “a part of,” because the subject matter greatly overlapped with what I’m interested in and what I write about here. There are various combinations of testing conferences, devops conferences, and formal methods conferences, sure, but this still felt like a new stake…
The Collatz conjecture is the prime example of the limitations of thinking in terms of branch coverage. It can be written as a recursive function in 5 lines of code with only three branches. That’s great, except we have no idea if it’s true or not, and no amount of tests can prove either way.
System performance boils down to the timing behavior of various interacting queues. Queues are one of those incredibly simple but powerful concepts, but they have some unintuitive or non-obvious behavior when only thinking about them mathematically. Simulating queueing scenarios gives us a better picture about how queues operate in practice.
We have to constantly wrestle with nondeterminism in tests. Model-based tests present unique challenges in dealing with it, since the model must support the implementation’s nondeterministic behavior without leading to flaky failures. In traditional example-based tests, nondeterminism is often controlled by adding stubs, but it’s not immediately clear how to apply this in a model-based context…
Transaction isolation is the kind of thing that you learn about and it fills you with fear. Specifically, there are weak transaction isolation levels which allow some fairly unexpected behavior. Tools like Jepsen are used to test the general isolation guarantees of databases, but it’s pretty uncommon to check the application layer for issues related to isolation anomalies. These anomalies can…
Proof assistants are really fascinating tools, but the learning curve can be extremely steep. If you’re a programmer by trade and not a mathematician, this curve can be even steeper, because it’s not like programmers are doling out proofs left and right at work. One particular sticking point that I had trouble overcoming is the difference between forward vs. backward reasoning - proofs assistants…
When I first stumbled upon certifying compilation1, I was absolutely awestruck. I thought a compiler was a very specific thing, a translator from source to target language. But a certifying compiler goes further: it also proves its own correctness. My motto has become “most tests should be generated”, so this immediately seemed like a promising approach to my goal of improving the generative…
Traditional testing wisdom eventually invokes the test pyramid, which is a guide to the proportion of tests to write along the isolation / integration spectrum. There’s an eternal debate about what the best proportion should be at each level, but interestingly it’s always presented with the assumption that test cases are hand-written. We should also think about test generation as a dimension, and…
Recently, Tomorrow Corporation released this video of their in-house tech stack doing some truly awesome time-travel debugging of a production-quality game. You should watch this video, even if you don’t read this post, because the workflow that they’ve created is really inspiring. The creator kept bringing up the fact that the reason their tools can do this is that they have determinism baked…