Yes, although it's hard to make it scale in every case. What you're talking about sounds like the field of program synthesis[1], which uses SMT solvers (among o

Yes, although it's hard to make it scale in every case. What you're talking about sounds like the field of program synthesis[1], which uses SMT solvers (among other technologies) to generate code to some specification. I worked on a system[2] that used this sort of technique to optimize code for a weird architecture (GreenArrays' Forth-based chip[3]) and it was certainly much easier to implement than a classical optimizing compiler. Perhaps the most relevant example project here would be Rosette[4], which is basically a framework for easily writing synthesizers for different tasks. It would let you implement a description of your machine in Scheme (ie write a simple interpreter) and automatically generate a synthesizer for it that could compile programs in your language to formulas in a solver of some sort. [1]: http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-overview-notes.pdf http://www.cs.berkeley.edu/~bodik/cs294/fa12/Lectures/L1/L1-... [2]: http://jelv.is/chlorophyll.pdf http://jelv.is/chlorophyll.pdf [3]: http://www.greenarraychips.com/ http://www.greenarraychips.com/ [4]: http://homes.cs.washington.edu/~emina/rosette/ http://homes.cs.washington.edu/~emina/rosette/