You can just let the AI pick from a possible set of optimizations, rather than having it suggest the optimizations itself. There are a lot of optimizations that compilers could easily recognize but can't do because they'd be violating the standard.

More realistically you can use an AI to generate vaguely realistic PGO data (profile guidance is where the real speed comes from). This has already been done at least by researchers.

> you can use an AI to generate vaguely realistic PGO data (profile guidance is where the real speed comes from)

That's not a bad idea, but PGO is pretty limited. I'm thinking about things like rewriting a loop to use vector instructions; something which compilers are absolutely terrible at but ChatGPT is actually pretty good at.

PGO is limited if you are chasing throughput on really tight programs that spend most of their time in a small number of loops (preferably with textbooks written about them), but it's really useful if you have a bunch of branchy code that mainly does one thing but has to cater for other things too (compilers come to mind).

Enabling PGO when building the D compiler made it almost 50% faster on some parts of the test suite (and fairly reasonable big files at that) - speedup elsewhere was not as dramatic but still a tidy win.

50% is probably a pretty extreme case for PGO, but when rewriting code to use vector instructions instead of scalar often has a speedup between 2x and 4x. Both approaches are interesting is all I'm saying.

> have a solid system for validating that two pieces of code are equivalent according to the C abstract machine

What ideas do you have for doing that in anything under exponential time?

I don't have any, I haven't thought about it enough. However, the reason I think it might be interesting is that checking if something is a correct solution is often easier than coming up with a correct solution for a lot of classes of problems (assuming P!=NP and all that).

And maybe you can't make a polynomial time verifier which works in the general case, but maybe you can make a useful one which handles a lot of cases.

I'm pretty sure that program equivalence is undecidable, ie you literally can't write this validation pass at all. There's a C compiler (compcert) that is formally verified to preserve the semantic of its input C code down to assembly, but it takes a lot of human developed proofs in Coq to get there.