Programmers will be even more productive when someone comes up with TLA++, which...

hwayne · on Sept 28, 2022

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.)

pron · on Sept 28, 2022

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.

ryanklee · on Sept 28, 2022

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?

the-smug-one · on Sept 28, 2022

It's HN, have some fun.

boffinism · on Sept 29, 2022

It's HN, don't.