> it can never prove the code is working correctly (see halting problem). The halting problem doesn't say anything about whether a program could prove things a

> it can never prove the code is working correctly (see halting problem). The halting problem doesn't say anything about whether a program could prove things about another program, just that it can't do it for all programs. Lots of programs obviously do or don't halt, and you can prove it in a couple lines ("there's an infinite loop here and every execution will enter it" or "all the loops are bounded by constants" etc). There's nothing stopping an AI from noticing things like that just as much as humans can. For more complex programs it obviously gets much harder, but it's very hard for humans to prove things about programs too!