> The implementation of this DSL is two folds. In Coq, a run function gives an executable semantics of the computations. The existence of an executable semantic

> The implementation of this DSL is two folds. In Coq, a run function gives an executable semantics of the computations. The existence of an executable semantics is an improvement over other works which only give unrealized axioms for I/Os effects Also > We can also question the correctness of the compilation to OCaml, or whether the run function in Coq is faithful to the extracted code. We have no formal proof, but we designed the system with correctness in mind. So the `run` function lives in their general OCaml extraction DSL [0] and produces a provable semantics (the first fold) and an extracted OCaml program (the second fold) which are assumed today to be equivalent so that proofs on the first fold can be transported to properties about the second. The run function looks like Fixpoint run {sig : Signature.t} {A : Type} (call_backs : CallBacks.t sig) (mem : Memory.t sig) (outputs : list Output.t) (x : C.t sig A) : option A * CallBacks.t sig * Memory.t sig * list Output.t which looks like a pure model of mutable typed memory, continuations via callbacks, and message passing. [0] https://github.com/coq-concurrency/system https://github.com/coq-concurrency/system