When such a system encounters a statement it can’t evaluate it might ignore it, or hang, or crash, or break the stack and execute your malware as root –there’s no way to tell without specifically looking at (and testing) each different class of problematic statement the system could encounter.
Actually, type theory is poweful enough to prove that programs will never do any of these things, for all statements at once. People rarely bother to prove that their programs are correct, but only because it’s not usually worth the effort.
I often see formal verification enthusiasts make such claims, but as far as I can tell that’s like saying AIXI solves the problem of AI design. If you could do this kind of thing on real programs under realistic conditions we’d all be using formal proof tools instead of testing departments. Instead large companies spend billions of dollars a year on testing we all know is inadequate, largely because efforts to actually apply formal techniques to these systems have failed.
These real-world programs that no one is willing to use formal proof tools on are 2-5 orders of magnitude more complicated than the hypothetical proof checker under consideration would be.
Futile brute-force testing is preferred because so many of the people involved are unwilling or unable to adequately formalize their actual requirements.
It is technically true that the people involved are unable to adequately formalize their actual requirements, but that is because precisely formalizing their requirements is a problem much harder than human mathematicians or computer scientists have ever solved. All humans would be “unwilling or unable to adequately formalize their actual requirements.” Notice, for example, that mathematicians can’t precisely formalize modern mathematics in the required sense either, and that problem is still much easier than formal verification for the sorts of things modern commercial projects are trying to accomplish.
Actually, type theory is poweful enough to prove that programs will never do any of these things, for all statements at once. People rarely bother to prove that their programs are correct, but only because it’s not usually worth the effort.
I often see formal verification enthusiasts make such claims, but as far as I can tell that’s like saying AIXI solves the problem of AI design. If you could do this kind of thing on real programs under realistic conditions we’d all be using formal proof tools instead of testing departments. Instead large companies spend billions of dollars a year on testing we all know is inadequate, largely because efforts to actually apply formal techniques to these systems have failed.
These real-world programs that no one is willing to use formal proof tools on are 2-5 orders of magnitude more complicated than the hypothetical proof checker under consideration would be.
Futile brute-force testing is preferred because so many of the people involved are unwilling or unable to adequately formalize their actual requirements.
It is technically true that the people involved are unable to adequately formalize their actual requirements, but that is because precisely formalizing their requirements is a problem much harder than human mathematicians or computer scientists have ever solved. All humans would be “unwilling or unable to adequately formalize their actual requirements.” Notice, for example, that mathematicians can’t precisely formalize modern mathematics in the required sense either, and that problem is still much easier than formal verification for the sorts of things modern commercial projects are trying to accomplish.