An AI smart enough should act like a senior engineer gathering requirements, it should start with assumptions and poke at different areas with questions until it has a complete idea, when I talk with a client I dont expect him/her to really formalize all the details its my role to question them until all the sharp corners are covered
Yes, but also, who do you gather requirements from? Other people. But if we're talking AGI, then these other people, i.e. users - or at least those who define the requirements - could be replaced, too.
> Certainly such an AI would be able to just write machine code directly and verify it through whatever means, including formal proofs, as needed. Why does it need a compiler?
If the AI can write the program bytecode through AI magic, why can’t it verify that it works through AI magic?
The AI needs a compiler for the program for same reason it needs a proof language to verify it.
We used to write programs without a compiler. We'd write them in Assembly. The AI won't even need the assembler. If verification is done through formal proofs, a logic language is, indeed, needed, but the program itself could remain in machine code.