Property Based Testing and The Cult of Typists

Created 2026-06-30, last modified 2026-07-21. Visibility: public

My relationship with types is... complicated. Languages without types (asm) or too stringly-typed (TCL) feel sloppy and fatiguing to use at scale, but I also find myself strongly disliking the work products of the "if some types good, more types better" mentality - and as I'll talk about later, I have my own atypical view of what a type ought to be, above and beyond the type systems we usually see marketed. What I find worth exploring lately, though, is that "strong" type systems have similar patterns of diminishing returns as Property-Based Testing.

So what is PBT? It's not really related to "properties" as the word was used in a lot of programming languages (fields within a record), it's more about characteristics. The classic example is addition. How would you test this function?

def add(a: float, b: float) -> float:
    return a + b

You might already have some conventional answers, but let's look at a PBT approach first and then loop around. One of the properties of addition is that it's associative: if you're adding a few things, the order doesn't matter.

def test_add_associative(a, b, c):
    assert add(add(a, b), c) == add(a, add(b, c))

Now, if you had a test harness that generated random numbers for a, b and c, which had a priority towards "edge case" numbers like +/- infinity, NaNs, etc., you could test points all over the number line, and catch a lot of failures without spending a lot of electricity on a high case count.

Of course, plenty of things are associative that aren't addition. Multiplication, for example. Right now, this totally bogus implementation would pass our tests:

def add(a: float, b: float) -> float:
    return a * b

To combat this, you can test for more and more properties to see that they hold generally, in situations you never consciously thought to check. Properties like reversibility:

def test_add_reversible(a, b):
    assert add(a, b) - b == a

This is kinda cool! You get to enforce multiple patterns of behavior across wide swathes of the input space. On the other hand, let's say that for our second test, we did something more conventional: a couple hand-chosen test cases where we know exactly what we expect.

def test_add_handpicked():
    assert add(0, 1) == 1
    assert add(1, 2) == 3
    assert add(-3, -4) == -7
    assert add(0.5, 0.75) == 1.25

This doesn't cover very much of the input space, but it covers a ton of the property space - quite a lot of behaviors on display here. With just one property based test and a handful of cases, we've made it very hard to contrive a bad implementation on purpose, let alone by accident.

This is why it's not really PBT versus conventional - the two can be combined to cover each others' weaknesses at an insane effort-to-reward ratio. Let's not, as they say, pit two bad bitches against each other.

Obviously, the examples I'm using here are intentionally trivial, but PBT really shines for complex functions under test. Consider a modern video codec - extremely complex, targeted by adversaries, and with performance pressure to be written in raw assembly. So, you write a clean, simple, assert-stuffed reference implementation with mostly or entirely conventional tests. Then you make a property test: "feed the same random input into the reference impl and the optimized impl, and check that you got the same answer." This isn't theoretical! The dav1d project, which is the fastest implementation of the AV1 video codec, relies on checkasm to verify parity between the outputs of reference code and platform-specific assembly. They also use fuzzing, which is just PBT checking for the property "does not crash," and some clever input generation to autodetect which possible inputs are most likely to be worth checking.¹

On the other hand, trying to test things with PBT only, and still have the tests in an adequate state, ends up being a long game of diminishing returns. Think about how many properties you'd need to define abstractly before you could really be sure that add(1, 3) == 4. And also, I've handwaved quite a bit about the cognitive and runtime cost of the harnesses for these things. Sure would be silly if we weren't using concrete values hand-in-hand, here!

Typemaxxing

Okay. So let's say there was an extremely popular tool within programming, which:

• was really good at enforcing some constraints across the entire input space,
• didn't always tell you everything you need to know,
• didn't enforce every property you care about,
• but could asymptotically approximate those missing pieces as you throw ever more effort at describing your constraints.

I know it sounds like I'm describing PBT. But am I? Or did I leave enough wiggle room in the constraints that they could be satisfied by something else? I'm "actually" (equally) talking about type systems!

Enough addition. Let's talk division.

def div(a: float, b: float) -> float:
    if b == 0:
        raise ZeroDivisionError()
    return a / b

Really, we have two possible outcomes, which we can fudge our way to thinking of as possible return types. Most of the time, we'll get a float, but sometimes we'll get an Exception. It depends on the zero-ness of b, but that's not in the type system. Let's make the type system a little smarter.

class NonZeroNumber(object):
    def __init__(self, val: float):
        assert isinstance(val, float)
        assert val != 0
        self.value = val

    # Various miserable glue to otherwise act numeric
    ...

Now we can communicate a constraint to the div function, and it can force us to check for zero-ness earlier, as a precondition!

def div(a: float, b: NonZeroNumber) -> float:
    return a / b.value

Well cool. Our new div function now has a more honest return type - it can't fail, so it's not actually implicitly float | Exception anymore. We can skip a check within the div function too, which is great for performance, as a single divisor value might be used for a lot of division operations, and now we can just check once up front.

Unfortunately, a can still be zero, so if you're chaining divisions, you're going to need to constantly re-wrap values in NonZeroNumbers. And, as commented in the example, these wrappers aren't ergonomically free, although some languages make them less painful with things like guard clauses or the ? operator. And zero-ness isn't the only property you may end up caring about, so you end up having to worry about how to communicate multiple traits of numbers: 2 is even, prime, an integer, greater than zero (and thus also non-zero), one of very few numbers where x*x == x+x, a power of two (which allows turning expensive divisions into cheap shifts), and probably ten other properties I'm failing to think of offhand. Which traits are worth checking ahead of time?

It's not that this technique is never useful, but it's never a free lunch either. Which means, as you solve more and more "properties of values" problems with the type system, the obvious wins will dry up, your typedefs will become too numerous to easily hold in your head, and you'll be paying the same costs or more to get the same benefits or less. The returns will diminish, and the line where the work stops being worth it is blurry and subjective.

Now, consider the following code:

average = div(a + b + c + d, 4)

If we inline the original div function, specializing it for the divisor of 4, we have such a bounty of information that an optimizer could turn this into a shift in just a couple steps.

average = (a + b + c + d) >> 2

That's the power of knowing a concrete value, which is specific enough to carry an absolutely massive bag of implicit properties. Neither div nor its caller really needs to find a way to talk about zero-ness or powers-of-two in a way that the type system understands, they don't have to coordinate with each other via a precondition enforcement system, it's just kinda... obvious.

The need for concrete data in order to understand and debug applications only scales with the subtlety of the constraints. Maybe you have a record type Person where .fullname needs to start with .firstname and end with .lastname². Is your type system expressive enough to enforce that? And if it is, what costs are you paying for that expressiveness? Some languages can handle this specific example very well, but then fall down for something differently subtle. And the more capable your type system becomes, the more it becomes a beast to learn in its own right, expensive at compile time, a fountain of contextually spurious errors, etc.

This is, of course, not some argument against ever using types at any level of granularity. If anything, the problem is that programming languages have a narrow idea of what types can be. The more expansive idea of what is a type? in my own head is "anything you could possibly think to assert about a value," whereas what most languages can actually enforce for you is limited to schema and layout. Type-y things I care about often vary wildly within the input space of language types, and can only be resolved against concrete values.³

While I have complaints about TypeScript, I find it fascinating that in order to retrofit schemas onto untyped data, they actually had to start treating concrete values like "some_string" as types themselves, such that the tag for a discriminated union might be "a" | "b" | "c". Prone's type system takes some cues from this!

This is also why C++'s constexpr is so powerful: it operates in the realm of concrete values. It can't prove that a function works correctly across all inputs, but it can prove the function works correctly across the inputs that actually get used:

constexpr int div(int a, int b) {
  return a / b;
}

int main() {
  return div(5, 0); // This will cause the build to fail!
}

Of course, programs operate on a lot of non-constant values too, in hostile environments full of data that won't be known until deep into runtime, which is exactly where types and assertions can help communicate and enforce: "this function can handle anything you throw at it, as long as it's in a shape we've declared support for." This is why Prone is a hybrid approach: moving computation into compile time reduces the burden on the type system, but you still have a type system, and it can be expressed/enforced with arbitrary assertions.