Verifying ReasonReact component logic — ReasonML & Imandra

Dave Aitken
Sep 10, 2018 · 4 min read
Image for post
Image for post

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!

Image for post
Image for post

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:

Image for post
Image for post

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 — 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?).
Image for post
Image for post
  • Currently Imandra can only be used via, 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!


Reasoning as a Service @

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store