Also you would probably want to cache the compiler's output in git because running that compiler would take a long time, and you probably want the compiler's output to still be inspectable to human inspection. In the end that compiled artifact would look a lot like source code.

I think Rust's success in the AI space shows how useful formal proofs are, as Rust provides something very similar to that. Both because it helps with the understanding of LLMs, as well as with trusting the LLMs are not violating any basic properties (like please no nasal demons if the user sends a buffer larger than the allowed amount).

We've got inform7 with an English like language generating complex inform6 OOP optimized code since a few decades and the i7 compiler might even run under a Pentium II with 128MB of RAM under NetBSD. I6, under 32 and a Pentium. And maybe even less. ZMachine games themselves (the biggest v8 ones) under the Frotz interpreter, under a 486 and 8MB (with FreeDOS and Frotz). Or maybe an Amiga or a m68k Mac with the same amount of RAM.

Now imagine what AMD64 machine can do with 2GB of RAM (minimum baseline for legacy, maybe some C2D computer) today.