It sounds nice for optimization in theory but in practice production compilers already have well oiled optimization pipelines that have mostly "flat" performanc

It sounds nice for optimization in theory but in practice production compilers already have well oiled optimization pipelines that have mostly "flat" performance characteristics (i.e. all the low hanging fruit is gone), and the algorithms are all very well understood because most of the fundamentals really haven't changed in ~20 years or more. The 80/20 rule mostly still applies. TBF this isn't always true. Unison[1] characterizes register allocation as geometric packing, a solution which is very robust on irregular architectures like Hexagon. GPUs have problems like extremely large register files that the literature doesn't treat very well which some solvers might help with, etc. And fully automated solvers are useful as complementary tools for any compiler, like Souper or Alive2. They're certainly good for specialized tools, especially validators. Personally, I think to prototype and construct a general program analysis quickly, you're better off with a tool like a Datalog variant. Souffle is pretty good. If you want to make generalized optimizers cheaper and more quickly, especially ones that can explore emergent optimizations that heuristics may not discover, solutions like equality saturation might be a better starting point[2] (it's kind of like a generalized version of a global cost-based SQL optimizer -- so the engine implicitly combines small rules together into more powerful rules.) Specialized solvers for particular logics or domains are still going to be valuable beyond that, of course. If you're writing a production compiler, your job is still cut out for you no matter what. If someone smart out there could "just" write an SMT solver and a robust Datalog that are efficient and easy to integrate as Lua ("drop in C files and go"), I'd fund that work. [1] https://unison-code.github.io/ https://unison-code.github.io/ [2] https://egraphs-good.github.io/ https://egraphs-good.github.io/