You may in fact be right, but I'm keeping away from neural network and AI/ML approaches for now. Part of my motivation here is as a crutch to human understandin

You may in fact be right, but I'm keeping away from neural network and AI/ML approaches for now. Part of my motivation here is as a crutch to human understanding - I want the system to be able to fail conclusively (i.e. "no such program at this size and with these assumptions exists" as opposed to "I couldn't find anything"). It's a lot easier to search for a 5-instruction sequence mentally if a computer has told you there _really_ is no 4-instruction sequence. This is a lot of compiler-type stuff, some bespoke optimizations and - like you say - tons of effort in pruning the search space. The backend to this is a SMT solver, but I have done a great deal of stuff to not get taken hostage by the mysteries of SMT solving (lots of tiny solves rather than handing huge parts of the problem to the solver). SMT solvers are great, and I encourage people to learn to use them, but they often need lots of domain-specific help. I do think that once I start bootstrapping our way up from short sequences to putting together bigger programs, there will be some AI-ish stuff happening. There are common patterns to how we put together programs that feel like they could be "learned" (after a fashion). The other big white whale here is to generate a program from a specification rather than from a black box. At the moment the superoptimizer can only make a better version of something that already exists. I do have a few ideas here, too, but there's a stretch goal.