The good intentions of the programmers are still necessary, and assumed, beyond the parts that are proved; and doing the proof work doesn’t make the whole process absolutely certain, but if you don’t strengthen certain parts of the process using logical proof then you are guaranteed to fail. (This failure is knowable to a competent AGI scientist—not with absolute certainty, but with high probability—and therefore it is something of which a number of would-be dabblers in AGI maintain a careful ignorance regardless of how you try to explain it to them, because the techniques that make them enthusiastic don’t support that sort of proof. “It is hard to explain something to someone whose job depends on not understanding it.”)
I expect if there were an actual demonstration of any such thing, more people would pay attention.
As things stand, people are likely to look at your comment, concoct a contrary scenario—where *they don’t have a proof, but their superintelligent offspring subsequently creates one at their request—and conclude that you were being over confident.
I expect if there were an actual demonstration of any such thing, more people would pay attention.
As things stand, people are likely to look at your comment, concoct a contrary scenario—where *they don’t have a proof, but their superintelligent offspring subsequently creates one at their request—and conclude that you were being over confident.