I’m not sure it’s just a matter of what we know right now, it’s mathematically provable that you can’t create a program which can find all security flaws or prove any provable code so bugs are pretty much inevitable no matter how advanced we become.
The theorem you cite (provided I understood you correctly) does not preclude the possibility of checking whether a program written in a certain pre-specified format will have bugs. Bugs here are defined to be certain undesirable properties (e.g., looping forever, entering certain enumerated states, etc).
Baby versions of such tools (which automatically check whether your program will have certain properties from inspecting the code) already exist.
If the language and format you’re using is Turing complete then you can’t write a program which can guarantee to find all bugs.
If you limit yourself to a subset of features such that you are no longer writing in a format which is turing complete then you may be able to have a program capable of automatically proving that code reliably.
Static analysis code does exist but still doesn’t guarantee 100% accuracy and is generally limited to the first couple of levels of abstraction.
Keep in mind that if you want to be 100% certain of no bugs you also have to prove the compiler, the checker, any code your program interacts with and the hardware on which the code runs.
If you limit yourself to a subset of features such that you are no longer writing in a format which is turing complete then you may be able to have a program capable of automatically proving that code reliably.
I’m not sure it’s just a matter of what we know right now, it’s mathematically provable that you can’t create a program which can find all security flaws or prove any provable code so bugs are pretty much inevitable no matter how advanced we become.
The theorem you cite (provided I understood you correctly) does not preclude the possibility of checking whether a program written in a certain pre-specified format will have bugs. Bugs here are defined to be certain undesirable properties (e.g., looping forever, entering certain enumerated states, etc).
Baby versions of such tools (which automatically check whether your program will have certain properties from inspecting the code) already exist.
If the language and format you’re using is Turing complete then you can’t write a program which can guarantee to find all bugs.
If you limit yourself to a subset of features such that you are no longer writing in a format which is turing complete then you may be able to have a program capable of automatically proving that code reliably.
Static analysis code does exist but still doesn’t guarantee 100% accuracy and is generally limited to the first couple of levels of abstraction.
Keep in mind that if you want to be 100% certain of no bugs you also have to prove the compiler, the checker, any code your program interacts with and the hardware on which the code runs.
Right, that is what i meant.