This was a lot more exciting than I expected.

The homepage does not do a very good job of explaining what we're looking at:

It appears to be a combination of two things:

1) A formalization of the Python language

2) An LLM which hooks into running programs and hot-swaps code with verifiably-equivalent behavior but better runtime performance, found via superoptimization and then verified via the formalization rules

This is brilliant, and in hindsight one of those "I can't believe nobody had thought of this yet" sort of things.

> This is brilliant, and in hindsight one of those "I can't believe nobody had thought of this yet" sort of things.

Please speak for yourself. We've seen many such ideas here even putting an LLM into a CPU to do branch predictions. Using it to write a (jit) compiler with correctness preserving transformations is not something that didn't occur to most compiler folks.

The intersection of the above two points requires non trivial expertise (and note that point 2 requires different low level expertise for the “swapping” part and the “optimization” part)