4 ms·

TLA+ is fantastic. Knowing it is like having superpowers. While others are mortally afraid of concurrency, you just spec your system & go. It also gives a huge

TLA+ is fantastic. Knowing it is like having superpowers. While others are mortally afraid of concurrency, you just spec your system & go. It also gives a huge decrease in cognitive load when you're implementing your system against a TLA+ spec. The hard stuff is already done. You can just glance at the spec to see what preconditions must be checked before an action is performed. No pausing halfway through writing a function as you suddenly think of an obscure sequence of events that breaks your code.

polskibus 9y ago
Are there any good tools around like c# codegen or verifiers?
- a-saleh 9y ago
  Last time I asked aound this, the replies I got were roughly: 1. this is not the focus of TLA 2. TLA is for high-level protocol specification, there probably wont be 1 to 1 mapping to code But I know i.e. some AWS team used TLA in their project, and I would like to finde their workflow, because it is not really clear to me, how do you usually get from "This spec checks out" to "I have a working code"
  - ahelwer 9y ago
    You translate it yourself ;) you're a programmer, go program! More seriously, the main classes of bugs TLA+ defends against are logic hole bugs and concurrency bugs - spec/design bugs, the most insidious kind! That's what AWS used it for; there is no machine-enforced correspondence with the code. People get really hung up on this, but after they try to formally verify something they see the wisdom of the separation. Proving code correct is extremely time-intensive. In contrast TLA+ gives you great bang for your buck. And to repeat - translating a TLA+ spec to code is not an error-prone process and is well, well within the grasp of software engineers.
yodsanklai 9y ago
You make me want to give it a try. How does it compare to tools like Spin? I remember trying Spin to specify a distributed system I was working on but I didn't find it as useful as expected. If I remember well (maybe not as it was a while) the built-in concurrency model didn't really match what I was doing in my program or my programming language. It turned out my model was too far from my program to be really useful.

polskibus 9y ago

Are there any good tools around like c# codegen or verifiers?

a-saleh 9y ago
Last time I asked aound this, the replies I got were roughly: 1. this is not the focus of TLA 2. TLA is for high-level protocol specification, there probably wont be 1 to 1 mapping to code But I know i.e. some AWS team used TLA in their project, and I would like to finde their workflow, because it is not really clear to me, how do you usually get from "This spec checks out" to "I have a working code"
- ahelwer 9y ago
  You translate it yourself ;) you're a programmer, go program! More seriously, the main classes of bugs TLA+ defends against are logic hole bugs and concurrency bugs - spec/design bugs, the most insidious kind! That's what AWS used it for; there is no machine-enforced correspondence with the code. People get really hung up on this, but after they try to formally verify something they see the wisdom of the separation. Proving code correct is extremely time-intensive. In contrast TLA+ gives you great bang for your buck. And to repeat - translating a TLA+ spec to code is not an error-prone process and is well, well within the grasp of software engineers.

yodsanklai 9y ago

You make me want to give it a try. How does it compare to tools like Spin? I remember trying Spin to specify a distributed system I was working on but I didn't find it as useful as expected. If I remember well (maybe not as it was a while) the built-in concurrency model didn't really match what I was doing in my program or my programming language. It turned out my model was too far from my program to be really useful.