[adrianN]

"Optimal" compilation is actually harder than NP-complete. Because program equivalence is undecidable, finding a canonical "optimal" representation for a program can't be done in general.

[programLyrique]

What about superoptimization? For instance, Stoke (http://stoke.stanford.edu/) or Souper (https://github.com/google/souper). They will not find all optimizations of course, and program equivalence is undecidable indeed, but they are a good shot at optimal compilation, I would say.

[adrianN]

Just because a problem is undecidable that doesn't mean that you can't in fact solve it for a large set of interesting instances (maybe all instances you care about).

[MaxBarraclough]

It's decidable provided the problem-space is finite, right?

[adrianN]

Every finite problem is decidable in linear time because you can hardcode the solution.

[MaxBarraclough]

Right, meaning decidability isn't an issue for superoptimisation of many kinds of problems.

[FartyMcFarter]

What does that mean in practice though?

I can say that every finite computational problem can be solved in O(1), so if the universe is finite, all real problems can be solved in O(1).

This sounds great until you realise that the constant factors involved would overwhelm any practical instance of this strategy.