My book came out today, so I’m feeling very excited and very grateful to everyone who helped along the way. Check out the acknowledgments for my thanks to several members of this community in particular.
It’s about a new approach to software design in which functionality is broken into “concepts”, each of which is a kind of nanoservice – formally, a state machine with its own state and actions. And yes, concepts can be specified in Alloy! The book defines them informally since it’s not for a specialized audience, but I do mention in some explorations in the second half how to make the models more formal, and I also talk about using the new temporal operators of Alloy 6.
–Daniel