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.
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.