Constraint solving your UIs
What happens when you take a tool for reasoning about your code, and plug it into the UI of the very code that it’s reasoning about?
It turns out we can do just that. Our core product Imandra is a cloud-native automated reasoning engine for ReasonML and OCaml. Imandra has been primarily designed with formal verification of your code in mind, but part of its toolkit is a powerful constraint solver.
Here’s a simple example from an Imandra REPL session:
# type person = { name: string, age: int };# let beatles_names = [ "John", "Paul", "George", "Ringo" ];# let is_adult_with_a_long_beatles_name = (x : person) : bool =>
List.exists(((n : string) => n == x.name), beatles_names) &&
String.length(x.name) > 4 &&
x.age > 18;# instance((a_person : person) => is_adult_with_a_long_beatles_name(a_person));1 base ground recursive instance
Instance (after 3 steps, 0.038s):
let a_person = {name = "George"; age = 19}
[✔] Instance found.
module CX : sig val a_person : person end
We define a type and then ask Imandra to generate an instance of it where the passed constraint function holds true.
When invoked, Imandra interprets your code and constraint functions with their underlying mathematical semantics in order to solve the constraints (as
opposed to randomly generating values and subsequently filtering them).
We also get the generated value back as something we can compute with:
# CX.a_person.age;
- : int = 19# is_adult_with_a_long_beatles_name(CX.a_person);
- : bool = true
This REPL-based interactive workflow can be pretty handy for exploring and experimenting with your code and its functions as you’re writing it. But let’s kick things up a notch and visualise this another way.
Understanding your UIs
As well as using Imandra via the REPL, its core features are exposed via an HTTP API, so we can hook it up to the browser.
In previous posts, we’ve talked about verifying React component logic written in ReasonML as part of our Verified React project. Summarizing those posts briefly, we can write core UI logic as a ‘pure’ state machine that Imandra can reason about, then delegate to it from the reducer function of a React component shell.
We can then ask Imandra for instances of our component state, and display that state instance in the UI component itself. Here’s an example of a TodoMVC app we’ve put together where we’re doing just that:
The input on the left is accepting our constraint function (the function we passed to instance in our REPL example), we then send it to Imandra over HTTP and render the returned instance via the UI.
We’ve pre-loaded a couple of helper variables and functions to help out with writing the constraints, but any expression based on the core logic would work — the rest of the generation is based purely on automatic analysis of the code of the component itself.
The final example constraint in the clip above also demonstrates how we can evolve the component’s initialState using its own update function, which can be useful for getting a visual handle on how things are working, and what particular actions do.
Currently when viewing component instances the component has to be modified very slightly so that the wrapping instance querying component can pass instances of the state through to it as a prop. Ideally we’d tap into the framework itself and inject the state in directly, and that’s something we want to look at next, but for now this shows the general idea pretty well!
You can try this example out by installing Imandra, cloning the verified-react repo and following the setup instructions in the README. There’s also another example of generating instances of TicTacToe in the same repo.
Constraint solving for profit
The previous example demonstrates using this setup to debug and analyse your components, but what about when the application you’re building involves constraint solving itself? We can leverage Imandra here again — rather than having to translate things into a format understood by the solver we’re using, we can write constraint expressions as predicate functions in ReasonML or OCaml, and let Imandra do the heavy lifting.
Here’s an example of that as part of a mini seating planner app:
Pairings define either whether people are indifferent to each other (neutral face), want to sit next to each other (happy face), or want to sit apart (sad face), and the visualisation below shows the table assignments for each person.
As the variables involved in the constraints are changed by toggling the UI, we send them up to Imandra as they’re changed. Imandra loads them in, and they’re examined alongside a pre-loaded constraint function to generate instances of valid seating arrangements. We then display these seating instances in the UI.
There is naturally a bit of overhead in the translation from code to raw
constraint expressions, vs hand written constraint expressions written with your domain in mind, but we can play around with different ways of expressing the same constraints to find the most optimal approach. However even a naive encoding can be a great starting point when experimenting.
What’s next?
As well as generating instances and verifying your code, Imandra can also decompose the state space of your programs, and we’re starting to look at applying this machinery to React too. By taking an initial UI state and the state machine definition, we’ll be able to use Imandra to decompose it, helping you visualise the possible future states of your components. We’re hoping this will be a great way to help developers spot edge cases and see how their apps evolve over time. Think along the lines of a time travelling debugger, but with the future as well as the past. 🤩
Watch this space!
If any of this sounds interesting to you we’d love to hear from you - come and chat with us in Discord, or check out Imandra. We’ll also be at ReasonConf in April, so come and talk to us there!
