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.
> You'd just work with them differently to get to the same ends, but with the added benefit of you can actually directly use the output of your efforts.
With TLA+ you can also directly use the output of your efforts. But if you're talking about compilation to some executable, that, unfortunately, requires a certain level of detail above which you cannot rise due to computational complexity concerns. So if you want that, you'd have to use TLA+ at the same level as other tools that emit code.
> 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.
Oh, of course! Those are excellent tools, but still niche (they target mostly embedded and/or real-time). You cannot use them to design and verify a 2MLOC system. I wasn't talking about popularity, but about target domains.
> 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.
First of all, as I said, it does not make a particular effort, because it's not necessary. People have used TLA+ to verify actual C, Java and Go code (that I know of). The problem is that once you do that you are bound by the scaling limitation of all tools that operate at that level. TLA+ is relatively special in that it can rise beyond that limitation, and that is where most of its users find value. Using TLA+ at the code level is just not using it to its full potential, and so misses the point. Unfortunately, specifying and verifying at that level can only be done by abandoning what we call "end-to-end", i.e. verification all the way to the code.
> 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 respects, but they deserve their due.
Of course, and I'm sorry if it sounded as if I was suggesting that TLA+ is better than them at what they do. I, myself, used Esterel decades before first learning of TLA+. TLA+ is better at other things -- things that are more applicable to a much wider application domain. My point is that due to fundamental limitations -- we can only verify a specification of a certain size -- there is an inherent tradeoff between scale and application domain and the ability to generate and executable.
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.