3 ms·

Godel's incompleteness theorem say that a system of sufficient complexity can not be bother complete and consistent [0]. Consistency ensures that statements can

Godel's incompleteness theorem say that a system of sufficient complexity can not be bother complete and consistent [0]. Consistency ensures that statements can not be both true and false (under a given set of axioms). Completeness says that everything that can be written down can be proved either true or false (under a given set of axioms). You must sacrifice one or the other. As we mostly care more about consistency (we don't want to make nonsense statements), completeness is sacrificed. Meaning, there will be things we can write down that we won't ever be able to prove true or false (relative to a set of axioms). There are many other implications and subtleties, like potentially not being able to show a set of axioms is complete or consistent, potentially not being able to show the equivalence of axioms, not knowing whether adding an axiom is still consistent, etc. Turing understood Godel's incompleteness theorem and applied it to computation. The computer science way of saying the above is that one can never make a program that can determine whether other programs halt or not (in finite time). Practically, this means that there will never be a compiler that will tell you whether you program has a bug. This is called the Halting Problem [1] and directly relates to Godel's incompleteness theorem as one can cast mathematics through the lens of computation and running Turing machines. Presumably the "classification" here is some combination of whether models are equivalent or consistent and complete. [0] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [1] https://en.wikipedia.org/wiki/Turing_machine https://en.wikipedia.org/wiki/Turing_machine

altruios 3y ago
one small detail to clarify. We can't build a general 'halting determiner' for any arbitrary program. But to say that for any particular program a halting machine can be developed is a different proposition. A simple example is the fact we don't have to run this code for ever to determine if it halts or not: ``` while(true){} ``` but we won't ever get a function() named X that outputs halt/not where x(turning machine / computer program). we able to, however, make a X(TM/C) where it outputs trivially halts or undetermined (past y steps).
- abetusk 3y ago
  Yes you're right. I should have said "it's impossible to create a program that, in general, for all input programs, determines whether it halts or not (in finite time)." The whole of mathematics and computer science is, in some sense, analyzing those programs which we can prove to halt.
irq-1 3y ago
> Godel's incompleteness theorem say that a system of sufficient complexity can not be both complete and consistent You've made an important and very common mistake of not qualifying this: it only holds true within the system. If you are using the same logical/mathematical system to evaluate its own completeness or consistency, then Godels results apply. Using other systems we can examine and understand the truth of sentences; which is to say, a systems completeness and consistency. Wikipedia includes this constraint: > For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. Few programmers and other on the internet understand the significance, often making reasoning about it wrong. > Practically, this means that there will never be a compiler that will tell you whether you program has a bug. TLA+ and other "external" systems can evaluate whether a program has a bug.
- hwayne 3y ago
  The GP had a few misconceptions about Godel and halting problems and stuff, but one nitpick here: >> Practically, this means that there will never be a compiler that will tell you whether you program has a bug. > > TLA+ and other "external" systems can evaluate whether a program has a bug. The main TLA+ model checker is TLC. It's pretty easy to write a TLA+ spec with a bug that TLC can't find (ironically by exploiting unbound model spaces, which are the Does Not Halt of model checking)
- abetusk 3y ago
  > You've made an important and very common mistake of not qualifying this: it only holds true within the system. It's not a mistake. I've stated it clearly. You're effectively qualifying it by saying you can add more axioms to extend the mathematical system to render previously incomplete statements complete. This comes at the cost of adding more incomplete statements. I can add the "The Riemmann hypothesis is true" as an axiom, say, and, assuming it's consistent with other axioms and actually adds some power that other axioms didn't, that might be fine, but this will create other statements that are also incomplete. > TLA+ and other "external" systems can evaluate whether a program has a bug. No, it won't. From the Wikipedia entry [0]: > The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired invariance properties such as safety and liveness. From this, at best this only does it out to a finite number of execution steps. I suspect this comes at the cost of exponential resources. So not only does it not find all bugs, the bugs it does find come at an increasingly intractable cost. [0] https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B

altruios 3y ago

one small detail to clarify. We can't build a general 'halting determiner' for any arbitrary program. But to say that for any particular program a halting machine can be developed is a different proposition. A simple example is the fact we don't have to run this code for ever to determine if it halts or not: ``` while(true){} ``` but we won't ever get a function() named X that outputs halt/not where x(turning machine / computer program). we able to, however, make a X(TM/C) where it outputs trivially halts or undetermined (past y steps).

abetusk 3y ago
Yes you're right. I should have said "it's impossible to create a program that, in general, for all input programs, determines whether it halts or not (in finite time)." The whole of mathematics and computer science is, in some sense, analyzing those programs which we can prove to halt.

irq-1 3y ago

> Godel's incompleteness theorem say that a system of sufficient complexity can not be both complete and consistent You've made an important and very common mistake of not qualifying this: it only holds true within the system. If you are using the same logical/mathematical system to evaluate its own completeness or consistency, then Godels results apply. Using other systems we can examine and understand the truth of sentences; which is to say, a systems completeness and consistency. Wikipedia includes this constraint: > For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system. Few programmers and other on the internet understand the significance, often making reasoning about it wrong. > Practically, this means that there will never be a compiler that will tell you whether you program has a bug. TLA+ and other "external" systems can evaluate whether a program has a bug.

hwayne 3y ago
The GP had a few misconceptions about Godel and halting problems and stuff, but one nitpick here: >> Practically, this means that there will never be a compiler that will tell you whether you program has a bug. > > TLA+ and other "external" systems can evaluate whether a program has a bug. The main TLA+ model checker is TLC. It's pretty easy to write a TLA+ spec with a bug that TLC can't find (ironically by exploiting unbound model spaces, which are the Does Not Halt of model checking)
abetusk 3y ago
> You've made an important and very common mistake of not qualifying this: it only holds true within the system. It's not a mistake. I've stated it clearly. You're effectively qualifying it by saying you can add more axioms to extend the mathematical system to render previously incomplete statements complete. This comes at the cost of adding more incomplete statements. I can add the "The Riemmann hypothesis is true" as an axiom, say, and, assuming it's consistent with other axioms and actually adds some power that other axioms didn't, that might be fine, but this will create other statements that are also incomplete. > TLA+ and other "external" systems can evaluate whether a program has a bug. No, it won't. From the Wikipedia entry [0]: > The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired invariance properties such as safety and liveness. From this, at best this only does it out to a finite number of execution steps. I suspect this comes at the cost of exponential resources. So not only does it not find all bugs, the bugs it does find come at an increasingly intractable cost. [0] https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B