Reasoning for days

Meet Verified React: The future of automated reasoning?

Eirini-Eleni Papadopoulou
© Shutterstock / VLADGRIN

What is the next step after ReasonReact? That would be Verified React, an application of automated reasoning to ReasonReact components. Let’s have a closer look.

Combining the power of a cloud-native automated reasoning engine and the work of the ReasonML/React community, Verified React is a project that aims to change the future of web UIs.

According to the team behind the project, Verified React is an application of automated reasoning to ReasonReact components for verification and symbolic analysis of their behaviors.

This project aims to make a significant impact on two key areas:

  • Symbolic verification vs. testing
  • State-space exploration

Although Verified React is still a work in progress, there are some milestones that have been reached. Let’s have a quick look at the progress so far.

Reasoning for days

Stage 1 of the development process for Verified React has been completed and it includes:

– Simpler automation of Imandra:

  • Added imandra-http-server as an alternative to imandra-repl to allow automation via an HTTP api, bundled with the Imandra installer.
  • Added bs-imandra-client – bucklescript bindings to that HTTP api to be used when running on Node.

– Allow export of export of core logic verified with Imandra to code that can be compiled to executable JS – Imandra comes with a prelude of pre-verified functions for use from .iml (Imandra-ml) or .ire (Imandra-reason) code.

– Automation of verification goals via jest, via imandra-http-server.

– Hook verified state machine up to React reducer component.

But that’s only the beginning. There are two stages still under development.

Stage 2

  • TodoMVC as a larger example
  • Displaying instances
  • Decomposition visualization

Stage 3

  • Collecting React reducer events from React unit test runs
  • Map reducer events back to state machine events, and visualize coverage on the decomposition
  • Coverage report of state space as hit by your jest tests

SEE ALSO: Build React.js routing using History API Fallback

Getting started

If you are interested in giving it a try, you need to make sure you have the latest version of imandra-repl installed via the Imandra Installer and then run:

You also need to make sure that all updates are installed so it can start up successfully. Once it’s started, quit it again with Ctrl-D and next you runnpm install in order to install the bucklescript compiler, imandra-prelude and Imandra client bindings for bucklescript and finally run npm run watch.

Check out the GitHub repo for all the relevant information.

Eirini-Eleni Papadopoulou
Eirini-Eleni Papadopoulou was the editor for Coming from an academic background in East Asian Studies, she decided that it was time to go back to her high-school hobby that was computer science and she dived into the development world. Other hobbies include esports and League of Legends, although she never managed to escape elo hell (yet), and she is a guest writer/analyst for competitive LoL at TGH.

Inline Feedbacks
View all comments