March 18, 2025

Verification-First Development

Or: why test-first development is not the same as test-driven development

A while back I argued on the Blue Site¹ that "test-first development" (TFD) was different than "test-driven development" (TDD). The former is "write tests before you write code", the latter is a paradigm, culture, and collection of norms that's based on TFD. More broadly, TFD is a special case of Verification-First Development and TDD is not.

VFD: before writing code, put in place some means of verifying that the code is correct, or at least have an idea of what you'll do.

"Verifying" could mean writing tests, or figuring out how to encode invariants in types, or adding contracts, or making a formal model, or writing a separate script that checks the output of the program. Just have something appropriate in place that you can run as you go building the code. Ideally, we'd have verification in place for every interesting property, but that's rarely possible in practice.

Oftentimes we can't make the verification until the code is partially complete. In that case it still helps to figure out the verification we'll write later. The point is to have a plan and follow it promptly.

I'm using "code" as a standin for anything we programmers make, not just software programs. When using constraint solvers, I try to find representative problems I know the answers to. When writing formal specifications, I figure out the system's properties before the design that satisfies those properties. There's probably equivalents in security and other topics, too.

The Benefits of VFD

1. Doing verification before coding makes it less likely we'll skip verification entirely. It's the professional equivalent of "No TV until you do your homework."
2. It's easier to make sure a verifier works properly if we start by running it on code we know doesn't pass it. Bebugging working code takes more discipline.
3. We can run checks earlier in the development process. It's better to realize that our code is broken five minutes after we broke it rather than two hours after.

That's it, those are the benefits of verification-first development. Those are also big benefits for relatively little investment. Specializations of VFD like test-first development can have more benefits, but also more drawbacks.

The drawbacks of VFD

1. It slows us down. I know lots of people say that "no actually it makes you go faster in the long run," but that's the long run. Sometimes we do marathons, sometimes we sprint.
2. Verification gets in the way of exploratory coding, where we don't know what exactly we want or how exactly to do something.
3. Any specific form of verification exerts a pressure on our code to make it easier to verify with that method. For example, if we're mostly verifying via type invariants, we need to figure out how to express those things in our language's type system, which may not be suited for the specific invariants we need.²

Whether "pressure" is a real drawback is incredibly controversial

If I had to summarize what makes "test-driven development" different from VFD:³

1. The form of verification should specifically be tests, and unit tests at that
2. Testing pressure is invariably good. "Making your code easier to unit test" is the same as "making your code better".

This is something all of the various "drivens"— TDD, Type Driven Development, Design by Contract— share in common, this idea that the purpose of the paradigm is to exert pressure. Lots of TDD experts claim that "having a good test suite" is only the secondary benefit of TDD and the real benefit is how it improves code quality.⁴

Whether they're right or not is not something I want to argue: I've seen these approaches all improve my code structure, but also sometimes worsen it. Regardless, I consider pressure a drawback to VFD in general, though, for a somewhat idiosyncratic reason. If it weren't for pressure, VFD would be wholly independent of the code itself. It would just be about verification, and our decisions would exclusively be about how we want to verify. But the design pressure means that our means of verification affects the system we're checking. What if these conflict in some way?

VFD is a technique, not a paradigm

One of the main differences between "techniques" and "paradigms" is that paradigms don't play well with each other. If you tried to do both "proper" Test-Driven Development and "proper" Cleanroom, your head would explode. Whereas VFD being a "technique" means it works well with other techniques and even with many full paradigms.

It also doesn't take a whole lot of practice to start using. It does take practice, both in thinking of verifications and in using the particular verification method involved, to use well, but we can use it poorly and still benefit.

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.