We run into the same kind of challenges to test programs with IO in Coq.io. To stay pure, we keep the IOs uninterpreted until the compilation (to an OCaml prog

We run into the same kind of challenges to test programs with IO in Coq.io. To stay pure, we keep the IOs uninterpreted until the compilation (to an OCaml program). We define the tests on the program with uninterpreted IOs. For clarity of the tests, we use an interactive debugger (reusing the tactical mode of Coq) to step through the IO operations. The main advantage of using Coq is that the tests can be made symbolic, thus covering a larger number of cases (if not all the cases). A simple example is explained here: http://coq.io/getting_started.html#use-cases http://coq.io/getting_started.html#use-cases (coincidentally, this is the same example as in this blog post).