Introducing Verified React
Over a relatively short time span, the web development community has re-engineered its software development process. Facebook’s React library (over 3 million downloads/week), has led to much cleaner architectural designs, and source code is much less error-prone and easier to reason about.
More recently, Facebook has followed up with ReasonML — another project that’s gaining a lot of momentum (scoring very favorably in 2018’s State of JavaScript survey given that the project is only a couple of years old). What’s very exciting is that the rigor and precision of source code written with ReasonML components allows the application of the latest advances in automated reasoning (symbolic AI/formal methods).
The following post will look over the recent milestones and demonstrate the underlying pattern and suggest the natural “next step” in the evolution of web development.
Automated reasoning
Here at Aesthetic Integration, the goal of our work is to help automate a lot of the error-prone manual tasks that developers/designers perform today. To power this automation, we’ve developed a powerful cloud-native automated reasoning engine (Imandra), allowing you to tap into the latest scientific advances in automated reasoning and formal verification. Recent headline-making hacks and their ensuing regulatory fines make the case for the value of these tools for us.
Now we’ve got our sights on the domain of web UIs. We call this project Verified React — combining the incredible work of the ReasonML/React community and our work on Imandra and its OCaml and ReasonML interfaces (check out https://try.imandra.ai).
Two areas where we hope Verified React will make significant impact:
- Symbolic verification vs. testing:
Testing, whereby developers write explicit sets of inputs/expected outputs, is an error-prone chore and is not natural to human beings. We think at a higher-level — in terms of symbolic behavior. What exacerbates the situation is that modern web applications have virtually infinite state spaces, making manual test case development even more onerous.
With formal verification, we can describe properties of programs symbolically and have machines analyze the underlying source code. With Imandra, we’ve built a powerful new automated reasoning engine equipped with a mechanized formal semantics of OCaml (and therefore ReasonML), allowing you to tap into the latest scientific advances in this field.
- State-space exploration:
React components are (virtually) infinite state machines. This is because state variables may contain rich, nested data structures, although even the basics like arbitrary strings and numbers represent huge numbers of ‘concrete’ states.
After you’ve written a component, it’s natural that you would like to explore how it may behave under the various possible scenarios that your code entails. In other words, what are the possible N-step state transitions of this infinite state machine?
Let’s now dive into Verified React in more detail. We’d love your feedback — please join us on our Imandra Discord!
Evolution of the front-end
After React’s release, developers quickly established various standard architectural patterns for their components and applications. Despite recent criticism of excessive boilerplate, frameworks like Redux (inspired by The Elm Architecture) have helped drive discussions and evolve application designs by making the application state more explicit and defining limited API to interact with it, saving developers a lot of headaches on large applications.
More recently, Jordan Walke — the original creator of React — and long time/prominent members of the React community have been working on ReasonML, which is based on the lightning-fast, statically typed OCaml toolchain (which has been around for 20 years, and is used in production by large organizations like Jane Street), but bringing it up to date with a syntax that’s more familiar to JavaScript developers.
ReasonReact — Reason’s React bindings — have been described as “React the way it was first intended” (it’s no coincidence that Jordan wrote a prototype of React in Standard ML at its conception). ReasonReact also embraces a Redux-like pattern out of the box in the form of the reducerComponent.
Ultimately, these developments and their incredibly quick adoption stem from the fundamental desire and need to write software in a way that makes it easier for coders to understand what their systems are doing and get a handle on their huge state spaces.
The reducerComponent helps makes all state and state-transformations explicit, and as a result a clear target for automated reasoning.
Symbolic verification vs Testing (Part 1)
The first thing we’ve looked at with Verified React is making it as easy to run logical assertions (or verification goals) against your application logic as it is to run a unit test suite. Verification goals are like tests, except assertions hold for the entire set of possible inputs, rather than just a single concrete test case. If you’re familiar with property-based testing and tools like QuickCheck the idea is similar, except verification goals are checked statically based on mathematical analysis of the state space of code itself. This also means you don’t have to write generators for your inputs (which QuickCheck requires), which can save a fair bit of effort.
We’ve put up a couple of examples in our Verified React repo — the first is the most basic example possible, a simple model representing a counter, with Increment and Decrement actions, and a couple of verification goals about the model. As an example (in Reason syntax):
This states that ‘for all models (the input to the goal function): when you send the Increment message, the model’s .count property is one higher than it was previously’. We can load this into Imandra as part of a Jest test. Note the difference from a unit test — we don’t actually have to come up with a concrete model and execute our code on it directly — Imandra mathematically analyses the code instead.
The second example is a bit more full featured — our model of the game TicTacToe. Again, we’ve got key properties of the game logic hooked up to be verified programmatically via a Jest test suite. If you’re interested in the workings of the TicTacToe model, read our other medium post, or check out the video we gave presenting it at the ReasonLDN Meetup — the walkthrough of the model starts about halfway through. We’ve hooked this verified model up into a full blown ReasonReact reducerComponent — you can play it here!
We’ll also be adding a third example — a model of a TodoMVC app with some verification goals, and a corresponding React wrapper, in the TodoMVC tradition of ‘showing how to use a thing to do something practical’.
State-space exploration
Next up we’ve got our sights on using Imandra’s symbolic reasoning to power some React-specific tools.
Within financial markets, we use Imandra to examine the state space of financial models — here’s a decomposition of a simple example specification of a FIX trading venue. You can browse the symbolic states of the venue and view samples for the input and output messages. Each symbolic state may represent many concrete states — for example, a state labelled x>3 could represent values for x up to infinity. Crucially, Imandra has proven that all values of x s.t. x>3 belong to the same ‘region’ of the state-space, i.e., the behavior of the model is invariant with respect to the choice of a concrete x satisfying that constraint. As such, when you view the messages, Imandra picks a concrete sample-point in that region (by solving the constraints), which can then be used as an actual input when executing the code of the model.
We can do something very similar with React reducerComponent logic, allowing visual and programmatic exploration of the state space, and allowing you to visualize your components in concrete instances of particular states to help discover and understand edge cases of the system that you may not have previously considered. Imandra can be used to automatically extend your test-suites (more on this below), to answer queries regarding possible behaviors, and to provide interactive exploration tools to understand and analyze complex edge-cases.
Symbolic verification vs Testing (Part 2)
Finally, we’re planning to hook into executing applications and record the messages passed to component update functions. With that information, we can analyze which states were hit during execution and allow you to understand state-space-based behavioral patterns (which regions of the state-space are hit most often? which are hit least often?). This can be used to isolate UI-unreachable regions, to help focus development efforts, and crucially can be connected to coverage metrics from the execution of a standard unit or property-based testing suite. Furthermore, Imandra can be used to query possible paths: “is it possible to reach state B from state A through a sequence of UI actions?”, and to extend a test suite by solving such queries for concrete event sequences.
Conclusion
We believe that with these tools in hand developers will be able to work on their code in a much more analytical way, giving them a lot more power during the development of their applications, as well as improve their overall quality.
We’re very excited about working on this stuff. If you are too, we’d love to chat. Join us on Discord or follow us on Twitter at @VerifiedByAI. Also, remember to take a look at the Verified React repo for much more discussion, the background of our plans, and the examples of what we’ve done so far.
Special thanks to Jordan Walke and Nik Graf for insightful discussions and feedback.
