Etat is a library for constructing finite state machines (FSMs) and statecharts (SCs) 1. Etat has the following design goals:
Etat also has the stretch goal of being able to construct an FSM or SC in Haskell and use that to generate code which implements it in other languages which have weaker guarantees. This allows you to use Etat to prove properties of the state-graphs of a system and then write the rest of that system in a different language, a bit like crux 2.
TODO -- see src/Etat.hs to see how we are playing around with this for now