3 ms·

TLA+ has no direct path to code. But it is a great way to test-drive your _idea_, to force you to dwell on your problem before beginning to code, to look for st

TLA+ has no direct path to code. But it is a great way to test-drive your _idea_, to force you to dwell on your problem before beginning to code, to look for states that you never thought about even in a simplified setting. Having gone through the exercise, I find I have greater clarity while coding, and have a better idea of where to place assertions and where to look for invariants. Often I iterate between prototyping with code, then playing with TLA+, then back to prototyping before throwing it all out and starting from scratch. ---- Then there are tools like Coq that convert a proof to running code automatically. For example, see the Verdi framework for doing Raft consensus: https://github.com/uwplse/verdi-raft https://github.com/uwplse/verdi-raft. This is clearly not for the faint of heart. The wonderful thing about this exercise is that it forces you to be precise about your specification, and holds your feet to the fire until your proof meets the spec. At the end of the day however, you have no guarantee that the specification (and the simplifications made to get coq going) are enough to capture enough interesting aspects of the real world. Still, for safety-critical and security-critical systems, it is always comforting that someone's gone through the pain of thinking it through to an extra level.

ternaryoperator 7y ago
Thank you for this explanation, without which I would have continued searching for a mirage. Everything makes a lot more sense now. It would be great if TLA+ made this clear (or at least clearer) right from the start.
pron 7y ago
TLA+ could, in principle, be used to directly verify code (e.g. [1]), and has been used like that "in the lab", but then it suffers from the same issues that all code-level, deep specification tools, like Coq, suffer from -- barely being able to get within three orders of magnitude from "ordinary" software. High-cost end-to-end verification of very small, very specialized programs by experts is a different practice altogether from low-cost, high-level design verification. TLA+ could be used for either, but the biggest bang-for-the-buck, especially in non-super-specialized cases is obviously the latter. [1]: https://tla2014.loria.fr/slides/methni.pdf https://tla2014.loria.fr/slides/methni.pdf
- sriram_malhar 7y ago
  I think that converting C to TLA+ is too low level; TLA's state space would explode before anything of consequence can be explored. There have been similar academic efforts to convert from SPIN's Promela to C, but nothing interesting has been shown. So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA. I think that a better solution is to have a DSL tailored to the domain, which can generate C for performance as well as a TLA+ model. Anil Madhavapeddy's PhD dissertation is a good example: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-775.html https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-775.html
  - pron 7y ago
    > TLA's state space would explode before anything of consequence can be explored You're confusing TLC with TLA+. TLC will work for small programs, but you can still use the TLA+ proof assistant (TLAPS) just as you can use Coq (and for the same definition of "can"). > So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA. TLA+ is not "too abstract". It is mathematics. It can describe a system at the level of general algorithms, or at the level of logic gates. In fact, it particularly excels at expressing abstraction/refinement relationships between descriptions of the same system at various levels. For example, you can establish a refinement from the C code to a higher-level spec with the proof assistant, and then use TLC to model-check the higher-level spec. But still, TLA+ is not likely to be any better than Coq, or any other deep specification and verification tool. Unfortunately, none of them can feasibly verify software of common size.
    - sriram_malhar 7y ago
      > You're confusing TLC with TLA+. True that. I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+. > TLA+ is not "too abstract". It is mathematics. I understand. I'd wager that is the chief reason why most programmers don't even begin to investigate it. Spin feels easier because it is operational and because it can incorporate C.

ternaryoperator 7y ago

Thank you for this explanation, without which I would have continued searching for a mirage. Everything makes a lot more sense now. It would be great if TLA+ made this clear (or at least clearer) right from the start.

pron 7y ago

TLA+ could, in principle, be used to directly verify code (e.g. [1]), and has been used like that "in the lab", but then it suffers from the same issues that all code-level, deep specification tools, like Coq, suffer from -- barely being able to get within three orders of magnitude from "ordinary" software. High-cost end-to-end verification of very small, very specialized programs by experts is a different practice altogether from low-cost, high-level design verification. TLA+ could be used for either, but the biggest bang-for-the-buck, especially in non-super-specialized cases is obviously the latter. [1]: https://tla2014.loria.fr/slides/methni.pdf https://tla2014.loria.fr/slides/methni.pdf

sriram_malhar 7y ago
I think that converting C to TLA+ is too low level; TLA's state space would explode before anything of consequence can be explored. There have been similar academic efforts to convert from SPIN's Promela to C, but nothing interesting has been shown. So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA. I think that a better solution is to have a DSL tailored to the domain, which can generate C for performance as well as a TLA+ model. Anil Madhavapeddy's PhD dissertation is a good example: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-775.html https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-775.html
- pron 7y ago
  > TLA's state space would explode before anything of consequence can be explored You're confusing TLC with TLA+. TLC will work for small programs, but you can still use the TLA+ proof assistant (TLAPS) just as you can use Coq (and for the same definition of "can"). > So, we have TLA+ on the one hand, which is too abstract, and C on the other, which is useless when translated to TLA. TLA+ is not "too abstract". It is mathematics. It can describe a system at the level of general algorithms, or at the level of logic gates. In fact, it particularly excels at expressing abstraction/refinement relationships between descriptions of the same system at various levels. For example, you can establish a refinement from the C code to a higher-level spec with the proof assistant, and then use TLC to model-check the higher-level spec. But still, TLA+ is not likely to be any better than Coq, or any other deep specification and verification tool. Unfortunately, none of them can feasibly verify software of common size.
  - sriram_malhar 7y ago
    > You're confusing TLC with TLA+. True that. I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+. > TLA+ is not "too abstract". It is mathematics. I understand. I'd wager that is the chief reason why most programmers don't even begin to investigate it. Spin feels easier because it is operational and because it can incorporate C.