Flamingo - Logic Programming Reborn for the Web
d4hines (3)

Hello!

UPDATE: with the team import issue resolved, we've moved the demo repl to our team: https://repl.it/@flamingolang/flamingo-todomvc-jam-submission

On behalf of @mbalduccini and myself, I'm very happy to submit Flamingo!

Flamingo's is an implementation of ALM, a logic programming language. Rather than writing algorithms that implement your domain logic with lists, loops, callbacks, etc., Flamingo allows you to express relationships directly, keeping the formal specification of your system as close to plain English as possible. However, unlike similar systems like Alloy, TLA+, Flamingo is designed to be executable - load it up into the browser and Flamingo will power the state management of your web app.

I've created a docs site here: https://flamingo-lang.org
It includes two tutorials that walk through the syntax and usage of the language.

Up to now, ALM has been mostly theoretical. Flamingo is the first practical implementation, and is the topic of my Master's thesis. My adviser, @mbalduccini, and myself are researching how Flamingo can be used to formally verify dynamic systems like web apps, robots, hardware, you name it. But our primary goal is making this process cheap - only when its easy to pick up the tools will formal verification become mainstream. In light of this goal, Flamingo is extremely minimalist - there are essentially on two constructs: if/then and given/when/then, respectively called state constraints and causal laws in the literature. On top of this, a simple but surprisingly rich module system allows for incrementally growing your systems.

As an example app, I've implemented TodoMVC in Flamingo: https://repl.it/@d4hines/flamingo-todomvc . Note - it doesn't seem to build correctly on Repl.it (runs out of memory), so I committed the build folder so you can see it without building - just hit start to run an http server.

Currently, Flamingo compiles to ASP, another, lower level logic language with SAT solving capabilities. My next goal for Flamingo however is to compile Flaming straight to Javascript via the techniques described in this paper: https://dl.acm.org/doi/10.1145/1552309.1552311 This will huge performance boosts and make Flamingo code ultra portable (essentially, Flamingo modules will compile down to dependency-free JS functions)

You'll note right away that performance is horrible. This is because Clingo, Flamingo's current backend, doesn't have a proper WASM api, and I load the whole binary on every user event.

While we've worked out sound algorithms, I didn't have time to implement the verification CLI that's mentioned in the tutorial.

I'm stoked for Flamingo's roadmap in the near future. First on the list will be implementing that Flamingo-to-JS compiler in a dependently-typed functional language (probably Coq, maybe https://github.com/moonad/formality). This will provide a rock-solid, ultra-high-assurance foundation, and open the door for producing certificates of correctness for Flamingo modules. Flamingo proofs can be produced automatically through SMT, so when this is done, Flamingo will be the easiest proof language in the world!

The next big issue is extending Flamingo to work with infinite domains like the natural numbers and integers. This is important for formal verification, but not a blocker, since no practical systems are truly "infinite".

Flamingo has been a blast to work on. We hope you like it, and we hope that it lowers the barrier for producing delightful and correct systems!

You are viewing a single comment. View All
TheDrone7 (1441)

@d4hines that will do. Thank you.