There is no such thing as provably secure software, and you should know that if you know anything about software security. The best you can actually do is prove that some particular exploit won’t work on your code, but there are always new classes of exploits out there waiting to be discovered. The space of possible inputs for any interesting program is far too large to explore, or even catalogue.
I think it is safe to say without further justification that you are wrong.
The same argument shows that I can never rule out the possibility that x^5 + y^5 = z^5 for naturals x,y,z, because the space of numbers is just too large. At best you can prove that some particular approach for finding solutions won’t work.
If by interesting program you mean, programs whose behavior shows no simple behavior which can be exploited by a human-understandable proof, then maybe your statement is tautologically true. But in that case, we definitely don’t need an interesting filter. We need a simple filter, whose behavior can be verified by a human proof.
If you are referring to the fact that we can never prove that our proof system is secure, then I guess I agree. However, I strongly, strongly believe that PA is consistent, and I am OK risking the universe on that assertion.
There is no such thing as provably secure software, and you should know that if you know anything about software security. The best you can actually do is prove that some particular exploit won’t work on your code, but there are always new classes of exploits out there waiting to be discovered. The space of possible inputs for any interesting program is far too large to explore, or even catalogue.
I think it is safe to say without further justification that you are wrong.
The same argument shows that I can never rule out the possibility that x^5 + y^5 = z^5 for naturals x,y,z, because the space of numbers is just too large. At best you can prove that some particular approach for finding solutions won’t work.
If by interesting program you mean, programs whose behavior shows no simple behavior which can be exploited by a human-understandable proof, then maybe your statement is tautologically true. But in that case, we definitely don’t need an interesting filter. We need a simple filter, whose behavior can be verified by a human proof.
If you are referring to the fact that we can never prove that our proof system is secure, then I guess I agree. However, I strongly, strongly believe that PA is consistent, and I am OK risking the universe on that assertion.