#(Coup d')Etat: Provably Correct Statemachines/Statecharts

Etat is a library for constructing finite state machines (FSMs) and statecharts (SCs) 1. Etat has the following design goals:

• provide an ergonomic DSL to construct FSMs and SCs;
• provide clear laws for FSMs, SCs, and their components;
• prove properties of FSMs and SCs at compile time via the type system.

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.

#Installation

TODO

#Usage

TODO -- see src/Etat.hs to see how we are playing around with this for now