The idea of provably safe AGI is typically presented as something that would exist within mathematical computation theory or some variant thereof. So that's one obvious limitation of the idea: mathematical computers don't exist in the real world, and real-world physical computers must be interpreted in terms of the laws of physics, and humans' best understanding of the "laws" of physics seems to radically change from time to time. So even if there were a design for provably safe real-world AGI, based on current physics, the relevance of the proof might go out the window when physics next gets revised.

I didn't get the impression that Eliezer's goal was to "build a provably Friendly AI" (in the mathematical sense of "provable"), as Ben puts it. The impression I get is more that Eliezer wants to put off building an AI until we understand enough about morality and human values. Eliezer also cares about mathematical proofs, but more for the purpose of preserving values under self-modification (something that humans don't usually have to deal with).

As an analogy, imagine you're trying to debug some complex and badly written code you were previously unfamiliar with. One approach is to find the bit in the code that seems related to the bug, and modify it locally ( "if DatabaseDown() return False" and the like) until the issue seems fixed. Another approach is to try to understand how the program works to the point where you understand which conceptual mistake caused the bug, and see the right way to fix it.

The second approach takes more time but is also less likely to create another bug somewhere else, or to deteriorate the overall quality of the code. I think most programmers who've worked on sufficiently large codebases have seen examples of both approaches.

Anyway, I get the impression that Eliezer is advocating something like the second approach here (understand how everything works before implementing), and that Ben is describing that as "proving correctness", which seems to be quite different (and much stronger!).