Oh and also what if everyone doesn't want to code in ocaml?
I think we need something similar but built on a type of ontology or description logics or something that represents the program in a common way that is not tied to a particular language representation or model. So I would start with research that does automated program generation in Ocaml and create a semantic model of those concepts.
You want to convert the functions from mirageos into this common knowledge representation in a way that integrates with the program generation ontology.
You then want to create a projectional editing system which allows for different representations including but not limited to ocaml.
Then you'd probably be looking for Cloudius OSv, which is written in C++ and runs mainly JVM apps (but is essentially the same idea). http://osv.io/