[bob1029]

> Software of this kind of complexity has all kinds of behavior that has never been broken

This space of things is astronomically larger than the space of things expressly covered by any test suite.

"Program testing can be used to show the presence of bugs, but never to show their absence." -Edsger W. Dijkstra

[w4der]

I've also seen situations where a customer reports a bug, the fix breaks some regression, and the updated behavior to work around the fix breaking the regressions turns into an undocumented feature.

[derdi]

How do you break a regression? A regression is breakage. Are you one of the people who use "regression" to mean "regression test"? Did Codex learn this from you? I hate it.

[w4der]

Yeah, sorry, it was a codebase with _only_ regression tests dating to the 80s, so we called everything a "regression".

[mbrock]

The same basically holds for proofs in the absence of coherent global correctness criteria like, say, confluence and normalization for a lambda calculus, or soundness and completeness for a logic.

Fable's napkin estimate of the effort required to produce a passable reference semantics for Postgres, which would involve novel discoveries in denotational semantics of concurrent transactions and so on, might be in the ballpark of 30–60 years of PhD level work.

So realistically I think the only way to validate a Postgres implementation involves differential testing, fuzzing, acceptance test suites, etc. And still you'll have bugs that need to be hammered out the good old fashioned way.