4 ms·
Nothing realistically complex can be proven "correct". There is even a mathematical theorem about it - given a program's code, one can't even prove that it ever
by EVa5I7bHFq9mnYK 3y ago
Nothing realistically complex can be proven "correct". There is even a mathematical theorem about it - given a program's code, one can't even prove that it ever stops.
One can, of course, apply proof of correctness to simple curcuits, where all possible inputs and outputs can be enumerated.
- Veserv 3y agoThat is a complete misunderstanding of consequences of Rice’s theorem which generalizes the halting problem. You can not prove non-trivial properties about all programs that could could ever exist with no false positives or false negatives. You can prove non-trivial properties about almost every program. For instance, if I want to disallow programs that will not halt, I can just reject any program with a unbounded loop. I may also reject programs with a unbounded loop that will halt, a false negative, but I do not care. I just want to be certain that I will never run a program that will not halt. I just decided: “will definitely halt for my purposes” even though the halting problem is unsolvable in general. This is generically true and is why formal methods work at all.