> I've often imagined automatically generating an efficient compiler backend via some sort of bruteforce or heuristic then verifying the code it generates via a

> I've often imagined automatically generating an efficient compiler backend via some sort of bruteforce or heuristic then verifying the code it generates via a theorem prover. Here's one paper that aims to do basically that, at the peephole optimization level: http://cs.stanford.edu/~sbansal/pubs/asplos06.pdf http://cs.stanford.edu/~sbansal/pubs/asplos06.pdf