Our achievement rests on two new results. First, finding a mapping from intermediate code to machine code is an undecidable problem. Second, using heuristic search, we can find mappings for machines of practical interest, in at most a few minutes of CPU time.
Our most significant new idea is that heuristic search should be controlled by algebraic laws. Laws are used not only to show when a sequence of instructions implements part of an intermediate code, but also as the primary heuristic for limiting the search: we drop a sequence of instructions not when it gets too long or when it computes too complicated a result, but when too much reasoning will be required to show that the result computed might be useful.
A crucial invariant of our search is that we consider only computations that we know can be implemented entirely by machine instructions. This invariant makes our algorithm significantly simpler than earlier search algorithms, which start with goal computations whose implementations by machine instructions are not known.