Verifying ReasonReact component logic — ReasonML & Imandra

We’re big fans of the OCaml ecosystem here at Aesthetic Integration, and our core product Imandra is tied closely to it — so we’ve been watching the development of ReasonML with interest.

As Reason syntax is implemented as a frontend to the OCaml compiler, we’re able to load Reason code into Imandra as if it were plain old OCaml code!

If you’re unfamiliar with Imandra, it’s a tool for analysing your code and mathematically verifying properties about it in order to help both understand what it does, and identify edge cases and bugs.

This description can sometimes sound a little bit abstract, so to illustrate we’ve written up an example in ReasonML to supplement the others available on our docs site.

The example

On the 4th of September, we demoed this example at the ReasonML London meet-up (video coming soon):

While Tic Tac Toe might not necessarily be the first thing that springs to mind when you think about ‘business logic’, we think the example illustrates how Imandra can analyse some of the often extremely complex and fiddly client-side logic backing frontend components and single-page applications.

We’ve taken some core logic for the game, and then wrapped it up in a ReasonReact frontend layer in order to produce a playable version — you can check out the ReasonReact project and core logic in this Github repo.

As part of the process of developing it, we loaded the definitions from the game logic into Imandra to aid development — a process which we discuss in our documentation site example writeup.

We use Imandra to verify a couple of properties of the game, including a key ‘game progression’ property:

This states that if we have a valid game, and a valid move, then playing the move on the game should produce another valid game. Rather than having to come up with different specific test cases and think of possible edge cases ourselves, Imandra generates these all for us based on our logical statement, and proves that it’s satisfied mathematically. As our initial implementation contains a small bug, Imandra finds a concrete counter example to help us figure out the issue:

We also use Imandra to generate example instances of the game’s data structures which satisfy certain predicates — if the game is being won, if it’s valid, etc.

The documentation can also be launched in a Jupyter notebook with Imandra loaded, on try.imandra.ai — you’ll be given an instance if you hit the ‘Try this!’ buttons throughout the docs, and you can experiment by changing the definitions and re-evaluating. You can also launch a fresh notebook with Reason syntax by hitting File > New Notebook > Imandra (ReasonML).

We’re hugely excited to be able to bring these tools to the frontend, and frameworks like React make it possible due to their functional nature.

What’s next for Imandra with ReasonML?

• The example currently verifies the core game logic — however there’s inevitably still some logic present in the mapping between the core and the React view layer. We’re hoping to build a stub of React in pure Reason or OCaml, that performs the same wiring as React without actually rendering anywhere (perhaps based on ReactMini in the ReasonReact repo?).

• Currently Imandra can only be used via try.imandra.ai, but in a few weeks we’ll be launching a client that can be downloaded for local development — watch this space! This should allow for both interactive workflows (helping you to develop your code in a REPL), but also give programmatic access to Imandra’s features so that verification goals can be run as part of a build, bringing you another weapon in your QA arsenal.
• We’re also working on Imandra VSCode plugins for both OCaml and Reason, supplementing the standard plugin features for each language with the Imandra keywords like instance and verify . We’ll then be iterating on the plugin to bring you inline counterexamples and verification goals displayed alongside your code as you’re developing with your usual tools.

Overall, we’re hugely excited about the future of the ecosystem, and looking forward to building (and verifying!) some awesome stuff!

We’ll soon launch a version of Imandra you can download and use locally, so stay tuned!