promotion of AlleAlle

[jurgenvinju]

@joukestoel I'd like to discuss the promotion of AlleAlle to a UseTheSource project here.

• link: https://github.com/cwi-swat/allealle
• it's a very general tool for use in DSL construction; namely it can be used to model and check all kinds of semantic relations and explore them using model checking without having to think about the nitty gritty details of SMT solving.
• it's written in Rascal, but it is also for Rascal's "one stop shop" meme
• it's used to implement Rebel2

Questions:

• Do you also see a future for AlleAlle in the coming 5 years?
• What other application areas are there in the foreseeable future for AlleAlle?
• What are pressing issues which need resolution in short term?
• Did I miss an important question to ask?

[joukestoel]

Yes! Supporting it would be a great idea I think!
I'll discuss the questions per bullet point:

Do you also see a future for AlleAlle in the coming 5 years?
Definitely. I think the language is a very suitable intermediate language for a wide array of problems. I see it as a Kodkod+ and seeing the areas where Alloy (and thus Kodkod) is used there is still great potential in the language (e.g. see for instance this list on the Alloy website)

What other application areas are there in the foreseeable future for AlleAlle?
Like I mentioned above, I think its application is very broad. I can easily imagine that it can be used in the live modelling / programming domain of @tvdstorm, @vrozen and Thomas van Binsbergen for finding all kinds of delta's. But is can just as easily be used as a backend for languages such as eFlint. I can even see that is could be used for some static analysis purposes. I think it's like Lego 😁

What are pressing issues which need resolution in short term?
The first one would be to actually register all known issues (to me) on its github page. I know that there are some bugs in the current implementation but I haven't registered them.
The other biggest "issue" I have with AlleAlle is that the translation to SMT is slow. I truly think that we should look at ways we could optimise the current implementation. This would enhance its applicability greatly.

Did I miss an important question to ask?
Not that I am currently aware but I will think about it

[jurgenvinju]

thanks @joukestoel ; so let's see what the others think.

[DavyLandman]

Who will take lead on support for this? Is Jouke committing for support in the future? Are there other members that could pick it up?

(I do think it's a useful addition, but I'm primarily asking the maintenance question)

[jurgenvinju]

That's an apt question Davy; I'm willing to support co-evolution patterns of Rascal (for example moving to the compiler and changes in the IDE support libraries) for this project, but I can not fix bugs in AlleAlle like @joukestoel can. I think some level of commitment would be required from you too Jouke. I would propose you take the lead.

[jurgenvinju]

BTW, AlleAlle UX support also depends on salix if I'm not mistaken.? I think we should not consider AlleAlle at usethesource before we also consider salix at usethesource.

[joukestoel]

Indeed good question @DavyLandman!
Since I will probably be a bit "further away from the fire" I can only promise you my best-effort. I am willing to support AlleAlle (since it feels like my brainchild :) but I do not know how much time is available to me to actually spend on it.

The current issues \ bugs in AlleAlle that I am aware of are fixable but will require some time to get right. So far, these issues haven't hindered my use of AlleAlle (they can be circumvented if you are aware of them).

[joukestoel]

Currently AlleAlle does not depend on Salix. It still uses the old visualization library. Upgrading its model visualizations to Salix is actually high on my wish-list for the project...

[jurgenvinju]

One the first new features would be (from the ING/Rebel side) to support more theories, in particular vectors and lookup maps; we might be able to allocate a masters' or bachelor student for a prototype of such a feature. @joukestoel is such a project feasible in the current implementation?

[joukestoel]

I think so.
The translation code has been setup with the addition of extra theories in mind. I think it would be / should be fairly straight forward to implement new theories.

Another great bachelor / master project would be to upgrade the visualisations of AlleAlle models. There is nice work on domain specific visualisations for Alloy (https://sterling-js.github.io/). Something similar could work very well for AlleAlle as well.