Pray, Mr. Babbage, if you verify the wrong properties, will the right answer come out?
Only some software is possible to verify, and there are many properties that it's impossible to verify because the software isn't the only thing that exists in the universe. No amount of mathematical proof on an ideal RAM machine will anticipate rowhammer.
And: just because something's theoretically possible, that doesn't mean an AI system would automatically pick up the ability to do it. Verifiable software in practice is still way behind what we currently know to be possible.
> No amount of mathematical proof on an ideal RAM machine will anticipate rowhammer.
you can infer algorithm failure rate depending on other input factors as an input. Say you found algorithm will fails every 10e15 years of continues run, you can accept such algorithm as reliable.
Only some software is possible to verify, and there are many properties that it's impossible to verify because the software isn't the only thing that exists in the universe. No amount of mathematical proof on an ideal RAM machine will anticipate rowhammer.
And: just because something's theoretically possible, that doesn't mean an AI system would automatically pick up the ability to do it. Verifiable software in practice is still way behind what we currently know to be possible.