4 ms·

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 w

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 8y 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.