It looks pretty impressive, but I’m struggling to find the practical problem it solves. Lots of jargon, eg “constraint language for modelling data structures”. How will that practically help making development easier / better / more secure?
It does bring a bit of a flashback to the GoF / UML craze of the 90es. UML supports visual constraint modelling, abstract state machines etc. The academic’s wet dream was being able to generate code from these abstractions to any language.
The big difference between Alloy and mainstream UML is that Alloy can check if your model has properties your want, and if not general a counterexample.
A couple use cases for this:
1. You're writing an access control policy feature. There are many different moving parts to it: you can assign policies to individuals or user roles, some resources can inherit policies from parent resources, some policies can have multiple conditions, etc. Is there some weird feature interaction that lets somebody see a resource they shouldn't?
2. You're modeling an invoice. Every invoice has a number of items, each item has a supplier. Some items may correspond to their own invoice the supplier is paying, with its own line items. Its possible for you to pay for an item by supplier S that corresponds to an invoice where they pay you. Also two suppliers may be able to supply the same item and have different invoices for that item. Does your model of this have any insane edge cases you should be worried about?
This isn't about generating production code, it's a way of testing designs. This helps shake out bugs in the design in much the same way fuzzing does in an implementation, but at this abstract level it's able to get much more exhaustive.
It's worth pointing out that Jackson wasn't specifically thinking of TLA+ when he wrote that. In _Software Abstractions_ he compares Alloy to B, OCL, VDM, and Z. TLA+ is very different from all of those, just as Alloy is. At some point in the future I'm supposed to write an in-depth comparison, though documentation work is higher priority right now.
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 tooling for, Lamport wanted a language that was easy to express complex logic in.
One consequence of this is that Alloy is a much smaller language: you can fit the entire syntax on a single sheet. It's also much easier in TLA+ to write a spec that you can't model-check, while with Alloy you have to be actively trying. It’s also impossible to write an unbound model in Alloy, so you’re guaranteed that every spec is over a finite state space. Which gets rid of the common TLA+ runtime problem of “is this taking a long time because it’s a big state space or because it’s an infinite state space".
Re tooling: Alloy converts to SAT, which makes model checking much, much faster. Specs that would take minutes to check in TLA+ take less than a second in Alloy. Being able to model-find as well as model-check is really nice, as is the ability to generate multiple counter/examples. The visualizer is really useful, too, especially for showing counterexamples to nontech folk. But the thing I honestly miss most when working in TLA+ is the REPL. It’s not the best REPL, but it’s a hell of a lot better than no REPL.
Okay, so drawbacks: Alloy doesn’t have an inbuilt notion of time. You have to add it in as a sequence sig. This means you can’t study liveness properties or deadlocks or anything like that. It also makes simulating concurrency awkward. This isn’t a huge problem if you have simple interactions or only one structure that’s changing, but the more “timelike” the problem gets, the worse Alloy becomes at handling it.
Less fundamental but still a big problem I keep having: no good iteration or recursion. Transitive closure is pretty nice but it’s not powerful enough. For example:
sig node {edge: set Node}
Is N1 connected to N2? Easy, just do `N1 in N2^.edge`. Through which nodes does N1 connect to N2? That's much harder.
The biggest problem with Alloy adoption, though, is social: there’s no comprehensive online documentation. If you want to learn it you have to buy _Software Abstractions_. Fantastic book but not something that’s especially convenient, and it doesn't cover newer features. We're working on changing this, but it will be a while before we have comprehensive online documentation available.
Which one is more appropriate to use really depends on your problem. As a very, very, VERY rough rule of thumb: TLA+ is best you're most interested in the dynamics of a system: the algorithms, the concurrency, etc. Alloy is best when you're most interested in the statics of a system: the requirements, the data relationships, the ontology, etc. My standard demos for showcasing TLA+ are concurrent transfers and trading platforms, while my standard demos for Alloy are access policies and itemized billing. You can use each in the other's niche, too (see Zave's work on Chord), so it's not a stark division.
This largely sums up my experience with Alloy and TLA+, as well as when I favor using one tool over the other. My formal education included classes in Z, so the spirit of Alloy always made sense to me and it's usually the tool I start with (I tend to see systems problems as relations, the tooling is fantastic, the REPL is very useful, counter-examples help illuminate the problem space, etc.)
When my problem is strictly algorithmic or it's all about the evolution of state spaces over time (especially concurrent states over time), I lean towards TLA+.
When my problem is strictly a state machine, I usually write out some combination of a Parnas table and a statechart, and then encode the table into Alloy.
I have a little tutorial I use to teach teammates the basics of TLA+ and Alloy, which takes about two hours to get through. I find that within a week of using Alloy, folks are dangerous enough to get value out of it.
My senior thesis was writing a transpiler from Alloy to SMT-Lib. I attended the Future of Alloy workshop with my advisor. Very intelligent, passionate group of people who care a lot about the language. I believe that its current primary use case is in education -- I remember one attendee described using the language to teach high school students first-order logic -- but its community hopes to further its use in industry as well.
I tried and failed to learn Alloy, the documentation is too mathematically dense for me, even though I suspect the concepts aren’t difficult for a working programmer.
Any tips on prerequisite knowledge are appreciated.
Likewise I searched in vain for one of these diagrams. It sounds interesting but the 'GUI' is just two text windows and a toolbar that look straight out of 1996 which doesn't bode well.
I mean, the first question in the FAQ is about those diagrams so maybe it should include an example of one? Usually when I'm evaluating a new project I am not so interested in figuring out what it can do if that isn't clearly communicated up front.
It does bring a bit of a flashback to the GoF / UML craze of the 90es. UML supports visual constraint modelling, abstract state machines etc. The academic’s wet dream was being able to generate code from these abstractions to any language.