As another comment also alludes, there's probably quite a lot more work required before this could be called a complete compiler (without heavy qualification as

As another comment also alludes, there's probably quite a lot more work required before this could be called a complete compiler (without heavy qualification as to what it actually compiles, since the language of boolean expressions probably isn't something that most people would consider to be a programming language per se); that said, toy languages like this are a great way to explore some fundamental principles of programming language theory. Boolean expressions have very trivial denotational semantics (since there's no recursion or state), so you could try formalising these in Coq (FRAP [1] and Software Foundations Vol. 2 [2] are both good places to learn more about this). Next, you could write formal operational semantics for your VM, and then finally prove that your compiler is correct in a formal sense (i.e. the image of any well-formed input under the compiler operation has a terminating execution in the operational semantics that yields the same value as would be obtained by the execution of the input expression under the denotational semantics). The last part would require implementing the compiler in Coq, but since you've written it in OCaml it probably wouldn't be very hard to port. [1] : https://frap.csail.mit.edu/main https://frap.csail.mit.edu/main [2] : https://softwarefoundations.cis.upenn.edu/plf-current/toc.html https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht... Edit: Having looked at your profile I now realise that you probably know all of this already, but it might be informative for anyone else reading :)