> But if it needs one language for programming, machine code, why is that the optimal and only one for every application? Why would any other specific language

> But if it needs one language for programming, machine code, why is that the optimal and only one for every application? Why would any other specific language be? Machine code is the most general and, as I said, if the AI wants to use a compiler to, say, help generate code for other platforms, it can create one. > Also predicate logic can be expressed using machine code It can't. Predicate logic has certain deduction rules, and these rules are different from those of machine code (e.g. machine code doesn't have quantifiers or their introduction and elimination rules). Of course, the AI could invent an ad hoc logic language and write a prover for it, but in this thought exercise, I think the point is that people would want to verify the proven properties (and possibly the implementation of the proof checker). > What’s easier: verifying the high-level matrix multiply to machine code lowering is correct (per machine) and therefore every application of it is correct; or that every single bespoke matrix multiply actually correctly implements matrix multiply for every machine? This isn't too relevant. If you need to build a skyscraper for tens of millions of dollars, you wouldn't spend much time thinking about how to lower the cost of the handle on the front entrance by $10. Even if every matrix multiplication is a little different, the proofs can be copied and changed slightly. The difference in cost of doing that or not is negligible compared to other aspects of the verification. Again, we write programs that are three orders of magnitude larger than the largest program we've ever managed to prove correct, and the difficulty does not scale linearly. So we're talking about an AI that's 10,000 or 100,000 times more capable than humans at writing software. Surely, matters as duplicating code and proofs are negligible for it. But even if it does matter, machine code isn't a problem because you don't have to duplicate manually. You can write the machine code that specialises the different applications and prove the correctness of that. This is like writing a small portion of a compiler. My general point is that proving arbitrary (practical) correctness properties of arbitrary (practical) programs is such a monumental achievement that anything more mundane, like a compiler, is trivial in comparison. It's like saying that someone can boil an ocean or move a mountain, but we must order them a taxi to get there.