Alloy is a language for describing structures and a tool for exploring them

Also a month ago: https://news.ycombinator.com/item?id=20909404

It's an excellent talk. I couldn't stop watching it.

https://www.cs.cmu.edu/~pattis/misc/socialproofs.pdf

A 2009 rebuttal to be fair to my side of the debate:

https://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=40...

Here's a recent article about the situation from yet another segment of people trying to bring in automation:

https://www.quantamagazine.org/in-computers-we-trust-2013022...

Unlike article's impression, a lot of how to build trustworthy provers has already been solved. The state-of-the-art is probably Milawa: a prover for ACL2-like logic running on a Lisp verified down to the machine code. It has summaries of various approaches of making computational math/logic trustworthy:

https://www.kookamara.com/jared/2015-jar-milawa.pdf

Note: Like in Common Criteria EAL7 or DO-178C, I'd use a mix of techniques for verification instead of blindly trusting the math. Lots of human review, static analysis, testing, etc.

Far as projects implementing math's foundations, you should especially check out Mizar (most complete) and Metamath (open source):

https://en.wikipedia.org/wiki/Mizar_system

https://en.wikipedia.org/wiki/Metamath

If authors give permission, it might be worthwhile to attempt to create re-writing tools that convert those tools languages into platforms in use by programmers. That's mainly Coq, the HOL's, Why3, and (hardware) ACL2. I don't know how feasible that is. I just think it could be valuable.

Has the original alloy gone unmaintained?

---

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}

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.

---

(Since writing that post, we're a few steps closer to having online documentation, and in the next couple of weeks or so I'll be running some first drafts past the rest of the team.)

Coq, by contrast, is a full theorem prover. I'm not experienced with it, but from my understanding it's mostly used in programming to prove things at a low level, where you're directly synthesizing code. Alloy is much higher level, relying on you to do the translations to code yourself. The upside is you don't need to know how to write mathematical proofs to use it, you just hit the "check model" button and it takes care of all of that for you.

If you want to see an example of Alloy in practice, I recently wrote a tutorial on using it to formally verify that your database migrations are safe: https://www.hillelwayne.com/post/formally-modeling-migration...

Coq is a proof assistant (and dependently typed programming language); more aimed at theorems.