Add a Formulog tutorial

[aaronbembenek]

We could use a nice introduction to the language. Optimally, it would build up to an interesting example Formulog program (such as a symbolic evaluator for a simple input language).

[bubaflub]

Hi, formulog folks! Would just like to add that I think this would be really helpful. I'm attempting to build out a system to model (computer) networks to answer questions about reachability (can Service A talk to Service B through some path?), security (are there any hosts that have port 22 accessible through the public internet?), and impact analysis (what happens if I change this firewall configuration?). I spent quite a bit of time reading through the docs, examples, and source code but I think a tutorial would have significantly sped up this process.

Perhaps it's because I'm not proficient in ML, datalog, nor SMT, but I think a few things to cover in more depth would be:

• The fragment of ML that is supported
• A better clarification on the two type systems
• What types of concepts should be modeled in datalog vs. what needs to be modeled in SMT and how to bridge the two
• Some examples of debugging during development beyond using print(...)
• Are there any limitations to what can be exported to souffle for compilation?
• Maybe some links to resources about the flavor of datalog that is supported and some more examples

I know this is a big ask but I think it'd help

[mgree]

Would it make sense to shoot for, say, a PLDI 2024 tutorial? Could be a good forcing function.

[aaronbembenek]

@bubaflub Thanks so much for giving Formulog a try and for your proposal of things to cover in a tutorial -- this is very helpful! I'll shoot to put a tutorial together sometime in early 2024. In the meantime, if you have any specific questions that are holding you back, feel free to raise them as an issue and we'll be happy to answer them.

Are there any limitations to what can be exported to souffle for compilation?

There shouldn't be: all features should be supported by the Formulog-->Souffle pipeline.

@mgree Looks like we've missed the tutorial deadline for PLDI'24, but maybe OOPSLA'24?

[mgree]

womp womp. sure, oopsla sounds good!

[bubaflub]

@aaronbembenek thanks! I'm prototyping something for $work and ran in to a few problems that were most likely my own poor understanding than anything wrong with formulog per se. Would you still like me to open up issues even if it's just a me-problem?

[aaronbembenek]

@bubaflub Absolutely! They might turn out to be Formulog issues; even if not, the discussion could be useful for others using Formulog.

(I will, however, be slow to reply for the next few weeks - my apologies in advance)