4 ms·

I'm now _really_ curious as to how many people who use and value TLA+ have actually used refinement. I've used it, you've used it, Lamport and (probs) Merz and

by hwayne 7y ago

I'm now _really_ curious as to how many people who use and value TLA+ have actually used refinement. I've used it, you've used it, Lamport and (probs) Merz and Markus have used it, most other people I've talked to haven't. Probably time for a community poll or something.

pron 7y ago
Technically it's impossible to use TLA+ without using refinement, as the entire TLA logic is based on it. Checking Machine ⇒ □P is checking that Machine refines □P. But, of course, the real power -- and what you and I both meant -- comes from writing machine formulas on both sides of the implication sign. I don't think many of those who use TLA+ use refinement between two machine formulas, but I think that's partly because they still consider TLA+ as a frontend language for TLC, which is unfortunate, because if all you want (or, rather, think you want) is a model-checker, there are probably better ones. In fact, the little use of refinement is just a symptom of this bigger issue. I don't think refinement is always useful, but I do think that everyone who uses TLA+ should use its power for analysis rather than just mundane model-checking. I admit, TLC is so enticing, that once you use it, TLA+ can feel secondary to it. Of course, I'd be happy if people used model-checkers more, whether TLC, Spin, NuSMV, Simulink or others, but I'd be even happier if people used TLA+ for its primary purpose, perhaps after being enticed by TLC: thinking about system design. I guess the problem is exactly what Lamport pointed out: programmers (including myself) don't like to think, especially when we can use automation. To be honest, I don't think I would have come to TLA+ if it weren't for TLC. So, in a sense, TLC both pulls people to TLA+ and obscures its main purpose. In the TLA+ workshop I imagine one day giving to my colleagues, I start with refinement. I would also start without TLC at all; just showing how TLA+ helps you think -- its main purpose and advantage. When writing specifications, I now always start with refinement, first writing how the system would behave at a very high-level, and only then refining a specific algorithm. (If anyone reads this without having read the article, and doesn't know what TLC is, it's a model-checker for TLA+ that's included in the TLA+ Toolbox)
- im_down_w_otp 7y ago
  Why exactly is TLA+ better suited to thinking about system design compared to say mCRL2, SCADE, or Simulink? Especially relative to the latter two since they provide a paved road to going from your system model to your system implementation, which TLA+ makes no attempt to do.
  - pron 7y ago
    I don't know mCRL2 at all, but SCADE and Simulink are niche tools (excellent at what they're for). TLA+ is completely general-purpose because it can describe a system at arbitrary levels of abstraction (and link the levels). You could hypothetically describe the same system at the level of logic gates or at the level of human interaction. Now, it is not true that TLA+ makes no attempt to directly link to the implementation, but it makes no particular attempt to do so. Its ability to do so stems directly from its power to describe a system at truly arbitrary levels. You want to describe your system at your code level so that you can verify your actual code? You can do that. But here's where things get interesting. If you want to verify a specification using any sound tool -- be it a model-checker or deductive proof -- the size of the specification becomes very limited. We can verify about 3000-6000 lines of a specification. It can be this number of lines of a low-level specification, i.e. code, or of a high-level specification. So this means that if we want to verify our actual implementation, our program must be tiny. But TLA+ gives you the option to specify and verify, say, a 2000-line high-level specification of a 2MLOC program to find problems at that level, and that's what people in general-purpose software need most. If your tool -- any tool -- links directly to the implementation, we know that the verified implementation will be very limited in size. It is TLA+'s ability to choose arbitrary levels of detail that gives it the power to help design large system. Such designs, however, cannot be formally (i.e. mechanically) linked to the implementation. If they could, we'd know how to fully verify large systems, but we don't.
    - im_down_w_otp 7y ago
      Everything you said about TLA+ here also applies to the other tools I mentioned. You'd just work with them differently to get to similar ends, but with the added benefit of you can actually directly use the output of your efforts. I also don't understand how you arrived at SCADE & Simulink being niche tools, but somehow TLA+ is general purpose? There must be at least 2 orders of magnitude more Simulink users doing model-based design & development than there are people who use TLA+ for pretty much anything. Simulink has limitations, but being comparatively niche relative to something like TLA+ isn't one of them. As an aside, not only does TLA+ not make an effort to provide a means of mechanically linking one's model to one's program, but when the question was asked of one of its progenitors how a developer might do this they were literally scoffed at for the suggestion. You're not describing anything to me that I'm not already aware of insofar as TLA+ is concerned. Having also used several other similar or adjacent tools, and being in constant contact with folks who use them for avionics systems, medical devices, large scale industrial automation, etc., I'm still inclined to say that TLA+ is fine. It's unnecessarily annoying in a bunch of dimensions. I am skeptical that if TLA+ wasn't descendent from one of the distributed systems godfathers, and wasn't associated with AWS in the software developer zeitgeist, that there'd be as much intrigue & interest around it. Also, I begrudge having had to come to the defense of SCADE and Simulink. I spend a non-trivial amount of my week essentially arguing against them in some respect, but they deserve their due.

by hwayne 7y ago

pron 7y ago

Technically it's impossible to use TLA+ without using refinement, as the entire TLA logic is based on it. Checking Machine ⇒ □P is checking that Machine refines □P. But, of course, the real power -- and what you and I both meant -- comes from writing machine formulas on both sides of the implication sign. I don't think many of those who use TLA+ use refinement between two machine formulas, but I think that's partly because they still consider TLA+ as a frontend language for TLC, which is unfortunate, because if all you want (or, rather, think you want) is a model-checker, there are probably better ones. In fact, the little use of refinement is just a symptom of this bigger issue. I don't think refinement is always useful, but I do think that everyone who uses TLA+ should use its power for analysis rather than just mundane model-checking. I admit, TLC is so enticing, that once you use it, TLA+ can feel secondary to it. Of course, I'd be happy if people used model-checkers more, whether TLC, Spin, NuSMV, Simulink or others, but I'd be even happier if people used TLA+ for its primary purpose, perhaps after being enticed by TLC: thinking about system design. I guess the problem is exactly what Lamport pointed out: programmers (including myself) don't like to think, especially when we can use automation. To be honest, I don't think I would have come to TLA+ if it weren't for TLC. So, in a sense, TLC both pulls people to TLA+ and obscures its main purpose. In the TLA+ workshop I imagine one day giving to my colleagues, I start with refinement. I would also start without TLC at all; just showing how TLA+ helps you think -- its main purpose and advantage. When writing specifications, I now always start with refinement, first writing how the system would behave at a very high-level, and only then refining a specific algorithm. (If anyone reads this without having read the article, and doesn't know what TLC is, it's a model-checker for TLA+ that's included in the TLA+ Toolbox)

im_down_w_otp 7y ago
Why exactly is TLA+ better suited to thinking about system design compared to say mCRL2, SCADE, or Simulink? Especially relative to the latter two since they provide a paved road to going from your system model to your system implementation, which TLA+ makes no attempt to do.
- pron 7y ago
  I don't know mCRL2 at all, but SCADE and Simulink are niche tools (excellent at what they're for). TLA+ is completely general-purpose because it can describe a system at arbitrary levels of abstraction (and link the levels). You could hypothetically describe the same system at the level of logic gates or at the level of human interaction. Now, it is not true that TLA+ makes no attempt to directly link to the implementation, but it makes no particular attempt to do so. Its ability to do so stems directly from its power to describe a system at truly arbitrary levels. You want to describe your system at your code level so that you can verify your actual code? You can do that. But here's where things get interesting. If you want to verify a specification using any sound tool -- be it a model-checker or deductive proof -- the size of the specification becomes very limited. We can verify about 3000-6000 lines of a specification. It can be this number of lines of a low-level specification, i.e. code, or of a high-level specification. So this means that if we want to verify our actual implementation, our program must be tiny. But TLA+ gives you the option to specify and verify, say, a 2000-line high-level specification of a 2MLOC program to find problems at that level, and that's what people in general-purpose software need most. If your tool -- any tool -- links directly to the implementation, we know that the verified implementation will be very limited in size. It is TLA+'s ability to choose arbitrary levels of detail that gives it the power to help design large system. Such designs, however, cannot be formally (i.e. mechanically) linked to the implementation. If they could, we'd know how to fully verify large systems, but we don't.
  - im_down_w_otp 7y ago
    Everything you said about TLA+ here also applies to the other tools I mentioned. You'd just work with them differently to get to similar ends, but with the added benefit of you can actually directly use the output of your efforts. I also don't understand how you arrived at SCADE & Simulink being niche tools, but somehow TLA+ is general purpose? There must be at least 2 orders of magnitude more Simulink users doing model-based design & development than there are people who use TLA+ for pretty much anything. Simulink has limitations, but being comparatively niche relative to something like TLA+ isn't one of them. As an aside, not only does TLA+ not make an effort to provide a means of mechanically linking one's model to one's program, but when the question was asked of one of its progenitors how a developer might do this they were literally scoffed at for the suggestion. You're not describing anything to me that I'm not already aware of insofar as TLA+ is concerned. Having also used several other similar or adjacent tools, and being in constant contact with folks who use them for avionics systems, medical devices, large scale industrial automation, etc., I'm still inclined to say that TLA+ is fine. It's unnecessarily annoying in a bunch of dimensions. I am skeptical that if TLA+ wasn't descendent from one of the distributed systems godfathers, and wasn't associated with AWS in the software developer zeitgeist, that there'd be as much intrigue & interest around it. Also, I begrudge having had to come to the defense of SCADE and Simulink. I spend a non-trivial amount of my week essentially arguing against them in some respect, but they deserve their due.