This seems as good a time as any for my mild rant about the formal modelling toolchain... A few things recently made me want to try out these techniques at wor

This seems as good a time as any for my mild rant about the formal modelling toolchain... A few things recently made me want to try out these techniques at work. Basically some issues we'd been facing, combined with reading Hillel Wayne's "Augmenting Agile With Formal Methods" blog post. So I read a little bit (I have no prior experience with any of this stuff) and decided to try out TLA+ First downer is I seem to have to download a 500MB Eclipse-based dedicated IDE to be able to follow any of the tutorials. Seems like a bad omen. Next I have the inevitable problem with wrong JVM runtime on my system... as ever, the "write once, run anywhere" promise pushes these issues down to the end-user rather than having the author compile working binaries for common platforms. https://github.com/tlaplus/tlaplus/issues/194 https://github.com/tlaplus/tlaplus/issues/194 No matter, solved easily enough. Ok so I'm stuck with a clunky unfamiliar IDE, but that's ok for now because to start out I will just be copy and pasting code from Hillel's beginner tutorial https://learntla.com/introduction/example/ https://learntla.com/introduction/example/ Within minutes I have put the IDE in an unusable state: https://github.com/tlaplus/tlaplus/issues/195 https://github.com/tlaplus/tlaplus/issues/195 At this point I'm thinking - these are just text files like any other language, why can't I edit them in my usual IDE and then run the model checker from the command line? This is technically possible. But this scenario is not well documented. You can download the tools from here https://lamport.azurewebsites.net/tla/tools.html https://lamport.azurewebsites.net/tla/tools.html The tools have no --help output explaining what args they need. They are not stand-alone command line tools either. They're just the source code, which you run directly against java. There is a .jar file available for download which might be some attempt at a packaged version of the tools, but who knows how to run it... Googling for instructions turns up this thread from 4 years ago, someone asking exactly this question, which goes unanswered https://groups.google.com/forum/#!topic/tlaplus/R9amI13F_-M https://groups.google.com/forum/#!topic/tlaplus/R9amI13F_-M ...the thread ends with a dismissive post from Leslie Lamport ridiculing such stupid ideas as having some documentation published on a website, and recommends everyone use the Toolbox IDE instead of trying to run the cli tools themselves. At this point it's quite clear to me why more people don't use TLA+, and it has nothing to do with the weird syntax or unfamiliarity with temporal logic. Since I still wanted to experiment with modelling I switched to Alloy. This also requires you install a dedicated (and rudimentary) IDE. At least this one actually works and I was able to experiment with some basic models of my own design. I could not see any stand-alone cli tools for Alloy but they do provide some basic instructions for using it programmatically in your own Java project http://alloytools.org/documentation/alloy-api-examples.html http://alloytools.org/documentation/alloy-api-examples.html (I'd prefer something accessible from Python, like a C library, but that's ok) I do understand that visualisation (Alloy) and presentation of complex results (TLA+) are an important part of the development process, and this is presumably what motivated both to provide via their own IDE. But clearly where the expertise on these teams lies is in the computer science, logic, model checker areas. Tying all of this brilliant and clever stuff to a cumbersome GUI app which is not your core proficiency to deliver seems like a very bad idea. A dose of the 'unix philosphy' would be beneficial I think. Think from the user perspective - I'd much rather use my usual IDE, which has great editing tools, a nice colour scheme, doesn't crash or become unusable, and is totally familiar and comfortable. Ok, it still needs a front-end for model-checking results... but imagine if the checker tool was well documented and provided structured output in a common format (json, graphviz .dot, whatever)... if these tools really are useful then I'm sure pretty soon you will have multiple front-ends created by people who are good at that. It seems sad to me that a small and brilliant community are wasting so much effort on making bad software, instead of making great tools which other people can build great software with.