4 ms·

One of the teams I worked for in AWS used TLA+ on a new back-end feature that was added. It was one that, if things went wrong, would be extremely bad for cust

One of the teams I worked for in AWS used TLA+ on a new back-end feature that was added. It was one that, if things went wrong, would be extremely bad for customers. The needs for operating on scale only added to the necessary complexity. Paranoia was key. They'd estimated something like an optimistic 4 months for the work. Two of the more senior developers were assigned the task, and they had to learn TLA+ and formal methods from scratch. (one dev's main complaint was that he was forced to use Eclipse, I don't know if integration has now happened with other IDEs since then). It took a little bit for them to get up to speed, but they were soon implementing and catching bugs in the proposed designs, and they had all the bugs ironed out within a few weeks. They then found that going from TLA+ to actual Java code was almost a "fill in the blanks" exercise. The formal model provided almost the exact structure they needed for their final code. Going from model to code took them very little time at all. It was in production, running in shadow mode after not even 2 months, and was fully live not long afterwards. TLA+ got subsequently used for a number of other features added to the platform. There had been general push back among developers that learning TLA+ and doing formal verification was only going to slow them down, but we found it was quite to the opposite. TLA+ actually sped up development, with the big bonus of higher confidence of correctness.

bordercases 7y ago
How do you believe using TLA+ compares to the "rich static typing" systems that pump up the valuations of Scala and Haskell?
- zozbot234 7y ago
  Not very comparable. TLA+ involves writing statements in a custom "logic" which adds modalities (i.e. monads) to support 'time' (or rather, state transitions in discrete steps, ala temporal logic) and non-determinism (which is reused to support refinement) to standard propositional logic. Nothing like this can be done in a standard programming language (even Scala or Haskell), and even in a dependently-typed language you would need to write some support code in order to embed this logic and work with it within the system. (It wouldn't be hard for sure, since even FOL gives you far more power than any (multi-)modal logic, but it's a different, perhaps more elegant take on things than just working directly within TLA).
  - bordercases 7y ago
    Thanks for your response.
hwayne 7y ago
> (one dev's main complaint was that he was forced to use Eclipse, I don't know if integration has now happened with other IDEs since then) There are a few projects to make this more accessible. We have vscode: https://github.com/alygin/vscode-tlaplus https://github.com/alygin/vscode-tlaplus Jupyter notebooks: https://github.com/kelvich/tlaplus_jupyter https://github.com/kelvich/tlaplus_jupyter emacs: https://github.com/mrc/tla-tools https://github.com/mrc/tla-tools I sort of wrote a vim plugin, but it's nowhere near as sophisticated as the above three. I also recently made public a personal CLI tool (https://github.com/hwayne/tlacli https://github.com/hwayne/tlacli) for running TLC on the command line. It's experimental but I find it really useful.

bordercases 7y ago

How do you believe using TLA+ compares to the "rich static typing" systems that pump up the valuations of Scala and Haskell?

zozbot234 7y ago
Not very comparable. TLA+ involves writing statements in a custom "logic" which adds modalities (i.e. monads) to support 'time' (or rather, state transitions in discrete steps, ala temporal logic) and non-determinism (which is reused to support refinement) to standard propositional logic. Nothing like this can be done in a standard programming language (even Scala or Haskell), and even in a dependently-typed language you would need to write some support code in order to embed this logic and work with it within the system. (It wouldn't be hard for sure, since even FOL gives you far more power than any (multi-)modal logic, but it's a different, perhaps more elegant take on things than just working directly within TLA).
- bordercases 7y ago
  Thanks for your response.

hwayne 7y ago

> (one dev's main complaint was that he was forced to use Eclipse, I don't know if integration has now happened with other IDEs since then) There are a few projects to make this more accessible. We have vscode: https://github.com/alygin/vscode-tlaplus https://github.com/alygin/vscode-tlaplus Jupyter notebooks: https://github.com/kelvich/tlaplus_jupyter https://github.com/kelvich/tlaplus_jupyter emacs: https://github.com/mrc/tla-tools https://github.com/mrc/tla-tools I sort of wrote a vim plugin, but it's nowhere near as sophisticated as the above three. I also recently made public a personal CLI tool (https://github.com/hwayne/tlacli https://github.com/hwayne/tlacli) for running TLC on the command line. It's experimental but I find it really useful.