4 ms·
Incompletness Theorem states that any system/language with primitive recursive arithmetic is either incomplete (since there is a construction of an undecidable
by fabianhjr 5y ago
Incompletness Theorem states that any system/language with primitive recursive arithmetic is either incomplete (since there is a construction of an undecidable statement via self reference) or unsound (since that same undecidable statement would be in contradiction)
AFAIK but speculating every programming language has primitive recursive arithmetic.
- gizmo686 5y agoYou are probably better off going with a computability theorem (such as the halting problem) instead of incompleteness. However, I suspect both will get you to the same place. Namely, there exists a program whose behavior cannot be predicted. There is no theory that says that there does not exist a program whose behavior can be predicted. We have just criminally underfunded research into formal verification; and somehow decided that even computationally limited, code is law programs handling millions of dollars don't need any type of formal verification
- carnitine 5y agoWhat does a standard programming language being unsound even imply? It’s not being used for theorem proving, so how is it of consequence?
- fabianhjr 5y agoThat it can produce contradictory results, if you have contradictions then at least one must be in error which means that following the language construction rules can produce erroneous results.
- UncleMeat 5y agoYou could imagine a semantics that produces different results depending on the order of inference rules.