On Monday, November 2nd, 2026 at 5:33 PM, Jeff Davis <[email protected]> wrote:
> On Mon, 2026-11-02 at 21:28 +0000, Greg Burd wrote: > > I would rather present a small, sound, reproducible core and grow it > > from there if there is interest. > > > > So, is there appetite for a PBT framework in the tree on these terms? > > If > > this is a non-starter, that is useful to know now. If it's worth > > pursuing, I'd like to hear from you. Hey Jeff, > Thank you for including a README, that's helpful. Thanks for taking a look at the README. > Right now it's about 4KLOC, which seems reasonable for a new testing > approach, if it's useful. Agreed, the first intro on the list was intentionally "bite-sized" so as to test the waters. > I'd suggest that we try to control the scope here. Some of these seem > like property testing for the sake of property testing. Again, just a demo at this point. None of the examples given were meant to illustrate how PBT pays off in practice within Postgres. The intention was to have very small examples to educate people on the concepts without distracting them with too many details. The sqrt bound is exactly the kind of thing I would drop before proposing a real set: it is a contrived property on a scalar function, and the README itself warns against inventing a formula to check a function. Point taken that the demo blurred the line. > +/* > + * sqrt bound: S = sqrt(abs(X)) is non-negative and, since numeric > sqrt rounds > + * to a scale, S*S must not exceed abs(X) by more than a small > relative-plus- > + * absolute tolerance. This is a sound one-sided bound: an exact sqrt > gives > + * S*S = X, and the only slack is the rounding of the last digit, well > within > + * abs(X) * 1e-10 + 1e-10. (The symmetric lower bound is scale- > dependent and > + * fiddly to state soundly, so we assert only the clean upper side > plus the > + * sign.) > + */ Yep, all those PBTs were basic examples I'd remove before offering up a solid set of real tests for commit. > It seems much more valuable to test, say, data structure invariants, > where we are likely to get creative with optimizations and might break > something. Is this property testing system good for that? Yes, and that is one area where I think it earns its place. I kept those areas out of the first cut to keep it bite-sized, but they already exist in the larger tree and are a better advertisement than the scalar ones: - binaryheap: build a heap from random inserts, then assert pop order is sorted, the first element is the minimum, and an incrementally-built heap matches one built in a batch. That is a pure data-structure invariant on binaryheap.c, no SQL involved. - btree / index scans: a differential oracle, an index scan must return the same rows as a sequential scan, over random tables, predicates, and index kinds (btree, gin, gist, partial, expression, multicolumn). This is exactly the "we got creative with an optimization and broke something" case you describe: the property doesn't know the right answer, it only knows the two paths must agree, so any divergence is a bug by construction. The three live bugs I cited in the first mail are all of that shape: an optimization computing a different result than the unoptimized path (SSI serialization, outer-join selectivity, MCV selectivity). Differential oracles over data structures and plans are the strong suit; the scalar round-trips are the warm-up. > Also, how do you see this affecting the dev process? Do most people > need to be aware of this framework, adding new tests along with > features? Or would most of the value come from adding lots of new > property tests in a big batch, hoping to catch some longstanding bugs? Good question, mostly the former. Today we have a few models for testing: regression tests pin exact output for a known case, TAP scripts a scenario, and isolation tests pin an interleaving. A PBT is a fourth model that sits alongside them, it pins a property that must hold across an input space the author can't enumerate by hand. It doesn't replace any of those; the README is explicit that a PBT belongs only where a disagreement is unambiguously a bug, and that a good unit test beats a contrived property. So no, most people would not need to think about it for routine work. The value concentrates where someone is doing something risky (a new scan optimization, a data-structure rework, a selectivity change) and wants a standing net under that specific area. The person making that change adds the property, the same way they'd add a regression test, because they know what invariant their change must not break. The big-batch "mine for longstanding bugs" mode does happen (that's how the three bugs surfaced), but I'd treat that as a bonus, not the pitch; the durable value is the standing differential net on the tricky areas, maintained by the people who work in them. > The timing of your proposal is not ideal, because AI is already finding > a lot of bugs, so finding more might be a thankless exercise until this > wave passes. So, if it doesn't get a lot of attention that may be the > reason why. I'd argue the opposite. This style of testing fits AI well: the properties are easy for an agent to write, cheap to run, and the counterexample the engine shrinks to is exactly the artifact an agent can consume to produce a fix, a minimal input plus a seed that replays it. An LLM alone can find bugs, but it does so by reading and reasoning, which burns tokens fast and doesn't reproduce, a property test is the opposite. The engine does the searching deterministically and cheaply, and the agent spends its tokens only on the one minimal case that actually failed. So I see PBT less as "more bugs to triage during the AI wave" and more as the scaffolding that makes the AI wave efficient, reproducible, and long-term helps collapse and manage that wave.. What I'm actually hoping people latch onto is using this as the foundation for harnesses that eliminate *categories* of bugs in tricky code, not one test per bug, but one property that rules out a whole class of bugs. Ideally the division of labor is: humans and LLMs write ordinary regression tests for the specific things they know a change must get right, and they write a property for the invariant that change must never violate. Then the engine, not the person, finds the input that breaks it. The human states the law; the machine hunts down the counterexample. That split is where I think the leverage is, and it's why I'd rather land a small sound core now and grow it than wait for the wave to pass. > Regards, > Jeff Davis best. -greg
