Last time I tried to use TLA+ I got very much repulsed by how hacky and amateurish it felt. I needed to use some ad-hoc GUI instead of my text editor, and some stuff had to be typed as comments in one language embedded inside another language that auto-generated the code outside the comment. That part was really gross. Not to mention the whole language looks like a pascal’s ugly cousin, which is superficial but just exaggerated the effect.
It’s really a shame, because I do understand the value proposition, and would wish to harness it. But if authors and fans want their ideas to be widely adopted, they need to make their software work like any other mainstream dev toolchains that developers are used to.
I would love to see “TLA+ for developer”, with a compiler, LSP, modern syntax, maybe even as a library on top of some mainstream programming language. If there is such a thing, or someone is aware of better approaches for the Unix hacker to get into it, I would appreciate it.
Last time I used TLA+, I added support for running the tools from the Emacs mode at https://github.com/mrc/tla-tools. Since there’s a TLA+ tree-sitter grammar now, I might add that next time I use TLA+.
I think that a unix hacker able to “understand the value proposition” could go past the innocuous idiosyncracies of TLA+. I mean, there’s a command line tool that has existed and worked consistently since far before LSP (and even possibly eclipse). Then there’s a fully functioning eclipse environment (so not a basic editor, even if it’s outdated). All this to write models that are usually less than 2 Kloc anyway. And in return you get one of the most important achievements in formal specification and verification of distributed algorithms.
There’s now a vscode plug-in you can use instead of the gui, and a C-style syntax for pluscal. Also, consider looking into Quint as a take on “modern tla+”
I’m mostly with you on this. I’ve used TLA+ in anger a few times with great results but it is definitely a weird experience using the tool.
If anyone reading this is genuinely considering putting the effort in on this… I do have one request: I, personally, enjoy TLA+ and don’t have much of an appetite for PlusCal. But what I would love is something that makes modelling state machines/state charts a little bit easier in TLA+. It’s totally doable as-is, all of the models I’ve built have been parallel-running state machines with message passing between them, but it sure feels like there could be an easier way to write them out.
Last time I tried to use TLA+ I got very much repulsed by how hacky and amateurish it felt. I needed to use some ad-hoc GUI instead of my text editor, and some stuff had to be typed as comments in one language embedded inside another language that auto-generated the code outside the comment. That part was really gross. Not to mention the whole language looks like a pascal’s ugly cousin, which is superficial but just exaggerated the effect.
It’s really a shame, because I do understand the value proposition, and would wish to harness it. But if authors and fans want their ideas to be widely adopted, they need to make their software work like any other mainstream dev toolchains that developers are used to.
I would love to see “TLA+ for developer”, with a compiler, LSP, modern syntax, maybe even as a library on top of some mainstream programming language. If there is such a thing, or someone is aware of better approaches for the Unix hacker to get into it, I would appreciate it.
Last time I used TLA+, I added support for running the tools from the Emacs mode at https://github.com/mrc/tla-tools. Since there’s a TLA+ tree-sitter grammar now, I might add that next time I use TLA+.
I think that a unix hacker able to “understand the value proposition” could go past the innocuous idiosyncracies of TLA+. I mean, there’s a command line tool that has existed and worked consistently since far before LSP (and even possibly eclipse). Then there’s a fully functioning eclipse environment (so not a basic editor, even if it’s outdated). All this to write models that are usually less than 2 Kloc anyway. And in return you get one of the most important achievements in formal specification and verification of distributed algorithms.
There’s now a vscode plug-in you can use instead of the gui, and a C-style syntax for pluscal. Also, consider looking into Quint as a take on “modern tla+”
Oh, Quint looks so nice. Thanks!
There’s also P (https://p-org.github.io/P/), I would be interested in hearing your opinion on that
I’m mostly with you on this. I’ve used TLA+ in anger a few times with great results but it is definitely a weird experience using the tool.
If anyone reading this is genuinely considering putting the effort in on this… I do have one request: I, personally, enjoy TLA+ and don’t have much of an appetite for PlusCal. But what I would love is something that makes modelling state machines/state charts a little bit easier in TLA+. It’s totally doable as-is, all of the models I’ve built have been parallel-running state machines with message passing between them, but it sure feels like there could be an easier way to write them out.