The current code base of Alloy started in the '90’s and has been worked on by a lot of very smart graduate students. Some of the code is absolutely brilliant but the age of the code base is clearly showing. Since Alloy started 30 years ago, a lot has changed. Java went from a bit more than a toy language to a half way decent one (really!). Today it has many concepts out of the box that had to be developed from scratch in Alloy. The code also shows that many generations of students worked at it for a short period; it is often surprisingly hard to find where something is happening. Worst of all, everything seems to be connected to anything.
Although I originally wanted to retire, I don’t use a lot of Alloy modeling anymore, Matthew Di Ferrante was willing to sponsor my work to do further improvements. One the first things we decided to do is to work out the actual grammar and create a new ANTLR parser based on modern technology. (The grammer can also be used in Python, JS, etc.)
For this sponsoring, i will take advantage of the work I did a long time ago: develop an (interface based) API on Alloy. A well defined API will make it easier to understand the Alloy code for educational purposes and simplifies building extensions. Most of the extensions over the last years have been retrofitted in with enormous effort. The Electrum port into Alloy 6 was an underappreciated herculean effort.
API based programming is something I worked on for most my life. It was the reason I fell in love with OSGi and it was the reason I fell in love with Alloy. For the OSGi I wrote thousands of pages of specifications and in retrospect I wish I had had something like Alloy. I am a sucker for concise clear crisp specifications and Alloy could make them verifiable. It was a bit of a surprise to me how the formal design community seems to highly focused on the proof aspect. For me a good Alloy model is worth a thousand pictures.
The reason that I am diving a bit deeper in the API topic is that I feel that Alloy itself could become an example of software engineering with formal methods. My good intention for this year is to continue the work with an Alloy model of Alloy. Anybody that is interested in this angle of Alloy should speak out so we can collaborate on it. Maybe universities that do software engineering and formal methods?
So how will this work go? The strategy of the current work is to not change the existing code base but insert an API between the parts. A Parser API, an AST API, a Solver API, a Visualizer API, a runtime API etc. For each API, a classic provider will created that maps the API to the classic code base. The classic code base might implement some interfaces but remains unchanged and compatible with today’s. However, once an API is in place it will become easier to plugin new implementations. However, all along the way we should remain 100% backward compatible although newer features might not work for older parts.
However, I think our direction should become language server oriented with VS Code as primary front end. This implies that likely little work will be done on the Java UI.
I plan to use this forum as a blog of my progress. I am already itching to tell you about all the nooks and crannies I found in Alloy’s sometimes magical syntax!
Peter Kriens