Earlier quoted context omitted.
Re TLA+, I'll copying my response from the last time Alloy was linked here: --- Alloy comes from the Z line of “systems are basically giant relational algebra problems”, while TLA+ comes from the LTL line of “systems are basically giant temporal logic problems”, which leads to a lot of fundamental differences between them. They also had different design philosophies: Jackson wanted a language that was easy to build t…
My undergraduate degree in CS covered Alloy, it was good fun to learn and solve problems with but I have to agree that the biggest pain point was definitely the limited documentation (even with access to the university's own resources). It's great to see improvements are on the horizon in this area! Edit: one of the other things I disliked about it was the GUI (it's Swing, IIRC). http://alloytools.org/workshop/slides…
Re: Alloy is a language for describing structures and a tool for exploring them
#21If you happen to remember some of the pain points, please let me know! I keep a list of the common pitfalls that I need to address in the docs.