I know you're being tongue-in-cheek... but this is actually something we care about a lot! There's a technique in formal specification called "Refinement", where you show a detailed spec successfully implements a more abstract one.

On the tooling side, Informal Systems has been doing some good work on static-typechecking TLA+ specifications: https://apalache.informal.systems/docs/tutorials/snowcat-tut...

(Disclosure, I've done consulting work for IS.)

TLA+ is not code but mathematics because that's what allows it to be arbitrarily expressive [1] so that (we hope) you can write a short and clear high-level description that is easy enough (with some study) to fully grasp and see if it is what you intended.

[1]: To the point where it can easily describe systems that can't be implemented in reality.

This is so snarky.

People are putting work into solving classes of bugs that cost us billions and billions in GDP per year.

This is one solution, and sure, like TDD, has tradeoffs and problems. The details, circumstances, and implementation all play a role.

But it's a potential way to go. Snark is not.

What's your solution?