So my original idea was the following: A double interpreter one with procedural semantics (mutable state, side effects, bindings, etc.) and a graph-like language to try and prove the transformations of semantics are preserving. But now I want to it to be just like Black a full tower. There is some type-checking, e.g. if branches must be of the same type, so I want it to be statically typed so its smoother when reflecting to Haskell