A couple of updates on this thread.
Thanks to advice from @rgrinberg, I was able to implement the feature-request of having dune load libraries of executables as well, and it has been merged into dune, I guess it will be available in the next release.
Separately, as some preliminary experiments in this direction, I’ve setup a basic extension to utop-mode that supports a Coq-like evaluation UI for OCaml:
If anyone wants to try it out and play with it, the source is here: