So, the story goes like this: I learned TLA+ to my best, but it doesn’t sparkle joy. I never wanted to program on LaTeX, or ever touch LaTeX for anything, really. And then I discovered Alloy.
Alloy is a formal verification language (and IDE for it) for describing categories of entities, relations between them, and constraints between these relations. For example you can have category User with relation follows to the set of users, and a user cannot follow themselves. That’s how you describe it in Alloy:
follows: set User
}
fact no_self_follows {
no u: User.follows {
u in u.follows
}
}```
That's it! There are shorter ways to describe the constraint, but this way is more similar to what you would do in Python. And, as you can see, it feels like a real programming language, and the syntax is quite nice.
When you describe your system, you can check different constraints on it (do the formal verification) or simply press "show" in IDE, and it will produce different graphs of the system that fits your description (with one and many follows, DAGs, loops, and so on).
It all doesn't seem like much, but, thanks to [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence), you can describe using it anything: types, sets, database records, servers, boolean logic, etc.
Alloy never was considered as an alternative to TLA+ because it didn't have temporal logic. But things have changed just a few years with introduction in Alloy 6 of even more cool temporal operators than TLA+ has. So, now I see Alloy 6 as a good replacement for TLA+ for myself that is developer-friendly, readable, more powerful, and easier to wrap my head around. Alloy does sparkle joy!
Learning resources:
+ [Finding bugs without running or even looking at code](https://www.youtube.com/watch?v=FvNRlE4E9QQ) (or [Alloy for TLA+ users](https://www.youtube.com/watch?v=tZywZc04lJg), it's the same talk for different audience) is a good intro video.
+ [Alloy Documentation](https://alloy.readthedocs.io/en/latest/index.html) is an unofficial documentation by Hillel Wayne about Alloy. At the moment of writing, it’s not updated for Alloy 6, so skip the "time" section. The rest is good.
+ As for TLA+, check out [the tag Alloy](https://www.hillelwayne.com/tags/alloy/) in Hillel Wayne's blog, it has some good posts. I especially recommend [Formally Modeling Database Migrations](https://www.hillelwayne.com/post/formally-modeling-migrations/) (doesn’t use time) and [Alloy 6: it’s about time](https://www.hillelwayne.com/post/alloy6/) (covers the new time syntax).