Nice. It reminds me of how compilers generate the optimal sequence of ADD+MUL for a division by a constant; in that case, the algorithm is simpler and has been synthesized in closed form, so the compiler can simply implement the logic (it doesn't need to "bruteforce" its way to it).

This is for instance Go's implementation which is readable and well documented:

https://github.com/golang/go/blob/master/src/cmd/compile/int...

Metalesson from whitequark is that they show us how we can be smart by rigorously applying existing wisdom. Esp by learning to use existing tools and taking advice from experts.

> My chosen approach (thanks to John Regehr for the suggestion) is to implement an interpreter for an abstract 8051 assembly representation in Racket and then use Rosette to translate assertions about the results of interpreting an arbitrary piece of code into a query for an SMT solver.

This appears to be a super-optimizer (https://en.wikipedia.org/wiki/Superoptimization) implementation, one of the smaller ones I have seen. Very cool!

What speedup over the human-written routines does this achieve?

At least a 1x speedup!

This looks like what CVC4's SyGuS component is useful for, especially since their optimization criteria is "smallest program"

Very cool.