In this report, the register machines use a very simple instruction set which we call the constree language. A full implementation can be found in Appendix B. However, when modelling concrete decision problems in Botworld, we may choose to replace this simple language by something easier to use. (In particular, many robot programs will need to reason about Botworld’s laws. Encoding Botworld into the constree language is no trivial task.)
From the technical report:
So next version will accept robot programs written in Coq, I suppose ;)