4 ms·
Programmers will be even more productive when someone comes up with TLA++, which will help you check if your TLA+ code has design flaws.
by owenpalmer 4y ago
Programmers will be even more productive when someone comes up with TLA++, which will help you check if your TLA+ code has design flaws.
- ryanklee 4y agoThis 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 4y agoIt's HN, have some fun.
- boffinism 4y agoIt's HN, don't.
- pron 4y agoTLA+ 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.
- hwayne 4y agoI 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-tutorial.html https://apalache.informal.systems/docs/tutorials/snowcat-tut... (Disclosure, I've done consulting work for IS.)