4 ms·

My original objection was to the claim that a non-trivial program could be demonstrated to be "provably correct." This statement is false. For non-trivial progr

by lutusp 11y ago

My original objection was to the claim that a non-trivial program could be demonstrated to be "provably correct." This statement is false. For non-trivial programs, it contradicts the simplest and most easily accessible interpretation of the Turing Halting problem and Gödel's incompleteness theorems, both of which demonstrate that this is not possible. Source: https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem Quote: "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." (emphasis added) > Multiple people have told you that you are simply factually wrong ... So as the number of people who object increases, the chances that I am wrong also increases? This is an argumentum ad populum, a logical error, and it is not how science works. Imagine being a scientist, someone for whom authority means nothing, and evidence means everything. In your next post, rise to the occasion and post evidence (as I have done) instead of opinion, or don't post.

catnaroek 11y ago
> My original objection was to the claim that a non-trivial program could be demonstrated to be "provably correct." This statement is false. For non-trivial programs, it contradicts the simplest and most easily accessible interpretation of the Turing Halting problem and Gödel's incompleteness theorems, both of which demonstrate that this is not possible. You don't need to solve the Halting problem (or find a way around Rice's theorem, etc.) to write a single correct program and prove it so. A-whole-nother story is if you want a decision procedure for whether an arbitrary program in a Turing-complete language satisfies an arbitrary specification. Such a decision procedure would be nice to have, alas, provably cannot possibly exist. To give an analogy, consider these two apparently contradictory facts: (0) Real number [assuming a representation that supports the usual arithmetic operations] equality is only semidecidable: There is a procedure that, given two arbitrary reals, loops forever if they are equal, but halts if they aren't. You can't do better than this. (1) You can easily tell that the real numbers 1+3 and 2+2 are equal. [You can, right?] The “contradiction” is resolved by noting that the given reals 1+3 and 2+2 aren't arbitrary, but were chosen to be equal right from the beginning, obviating the need to use the aforementioned procedure. The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them. Typically, this is only possible if the program and the proof are developed together, rather than the latter after the former. This much math you need to know if you want to lecture others on the Internet. :-p
- dllthomas 11y ago
  Very good analogy! > but were chosen to be equal right from the beginning While this was almost certainly the case, it's sufficient for them to have been chosen so as to be decidably comparable.
  - catnaroek 11y ago
    > it's sufficient for them to have been chosen so as to be decidably comparable. Indeed. :-)
- lutusp 11y ago
  > The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them. The system you outline works perfectly as long as you limit yourself to provable assertions. But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms, likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct. If we're balancing a bank's accounts, I think we're safe. In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy. > This much math you need to know if you want to lecture others on the Internet. My original objection was completely appropriate to its context.
  - catnaroek 11y ago
    > The system you outline works perfectly as long as you limit yourself to provable assertions. Of course. And if a formal system doesn't let you prove the theorems you want, you would just switch formal systems. > But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct. Programming is applied logic, not religion. And a proof doesn't need to be “believed”, it just has to abide by the rules of a formal system. In some formal systems, like intensional type theory, verifying this is a matter of performing a syntactic check. > If we're balancing a bank's accounts, I think we're safe. I wouldn't be so sure. > In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, I see this as more of a problem for specification writers than programmers. Since I don't find myself writing specifications so often, this is basically Not My Problem (tm). Even if I wrote specifications for a living, I'm not dishonest or delusional enough to charge clients for doing something I actually can't do, like specifying a program that claims to be an accurate model of the human brain. > and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy. I don't see what's so hard about sticking to program structures (e.g., structural recursion) for which convenient proof principles exist (e.g., structural induction). Please, get yourself a little bit of mathematical education before posting your next reply. You're so stubbornly wrong it's painful to see.
deleted 11y ago
[deleted]
dllthomas 11y ago
> "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." You seem to be mixing up where the "for all" lies. The result is: There does not exist a procedure that, for all (program, input) pairs, the procedure will say whether the program halts for that input. {p | Ɐ(f,i): p(f,i) says whether f(i) will halt } = ∅ You are using it as if it said: For all (program, input) pairs, there does not exist a procedure that will say whether the program halts for that input. Ɐ(f,i): {p | p(f,i) says whether f(i) will halt } = ∅ "post evidence (as I have done)" What is at issue is your incorrect assertions about what your evidence says. We read it, it contradicts you, everyone points this out, and you just ignore it and get louder.
- lutusp 11y ago
  > You seem to be mixing up where the "for all" lies. Not at all. My original objection was to the claim that a program could be proven correct, without any qualifiers. Any program, not all programs. As stated, it's a false claim. Your detailed comparison doesn't apply to my objection, which is to an unqualified claim. > everyone points this out ... Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing. > you just ignore it and get louder. I wonder if you know how to have a discussion like this, in which there are only ideas, no personalities, and no place for ad hominem arguments?
  - dllthomas 11y ago
    > My original objection was to the claim that a program could be proven correct, without any qualifiers. Any program, not all programs. Let's be precise. Let P be the set of all programs. Let C(s) ⊂ P be the set of programs correct relative to specification s. As I read the original statement, it was saying, {p ∈ C(s) | p, s ⊢ p ∈ C(s)} is large enough to be useful I am not sure whether you read it differently. > As stated, it's a false claim. You have said this repeatedly, but all you have done in support of it is point at the Halting problem. The Halting problem says: ∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts)) You have claimed this eliminates the possibility of proving correct any non-trivial program: > [T]he Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct." I see no way to read that but as a claim that: (∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → p is trivial) Please supply a proof. Note that it's quite true that (∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → *s* is trivial) proved usually by reducing s to "halts" for any non-trivial s. > Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing. I am not deciding it by poll. I am pointing out that there are objections to your reasoning that you have not addressed and persist in not addressing - despite them being made abundantly clear, repeatedly. > I wonder if you know how to have a discussion like this, in which there are only ideas, no personalities, and no place for ad hominem arguments? You're accusing me, as a person, of not understanding that a discussion like this has no place for accusations against a person? My complaint was not about you as a person, but about the form of your arguments in this discussion.
geofft 11y ago
> In your next post, rise to the occasion and post evidence (as I have done) instead of opinion, or don't post. I have already done so. Did you read my comment about existential vs. universal quantifiers? Can you respond to it? This was the original claim: > It's false -- the Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct." This is the statement you quoted from Wikipedia: > Quote: "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." Do you agree or disagree that the quantifiers in these two statements are different? Do you agree or disagree that "the Turing Halting problem demonstrates that one cannot establish that every single non-trivial program is either 'provably correct' or 'provably incorrect'" is a different claim than the one originally made?

by lutusp 11y ago

catnaroek 11y ago

> My original objection was to the claim that a non-trivial program could be demonstrated to be "provably correct." This statement is false. For non-trivial programs, it contradicts the simplest and most easily accessible interpretation of the Turing Halting problem and Gödel's incompleteness theorems, both of which demonstrate that this is not possible. You don't need to solve the Halting problem (or find a way around Rice's theorem, etc.) to write a single correct program and prove it so. A-whole-nother story is if you want a decision procedure for whether an arbitrary program in a Turing-complete language satisfies an arbitrary specification. Such a decision procedure would be nice to have, alas, provably cannot possibly exist. To give an analogy, consider these two apparently contradictory facts: (0) Real number [assuming a representation that supports the usual arithmetic operations] equality is only semidecidable: There is a procedure that, given two arbitrary reals, loops forever if they are equal, but halts if they aren't. You can't do better than this. (1) You can easily tell that the real numbers 1+3 and 2+2 are equal. [You can, right?] The “contradiction” is resolved by noting that the given reals 1+3 and 2+2 aren't arbitrary, but were chosen to be equal right from the beginning, obviating the need to use the aforementioned procedure. The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them. Typically, this is only possible if the program and the proof are developed together, rather than the latter after the former. This much math you need to know if you want to lecture others on the Internet. :-p

dllthomas 11y ago
Very good analogy! > but were chosen to be equal right from the beginning While this was almost certainly the case, it's sufficient for them to have been chosen so as to be decidably comparable.
- catnaroek 11y ago
  > it's sufficient for them to have been chosen so as to be decidably comparable. Indeed. :-)
lutusp 11y ago
> The way around the Halting problem is very similar: Don't write arbitrary programs. Rather, design your programs right from the beginning so that you can prove whatever you need to prove about them. The system you outline works perfectly as long as you limit yourself to provable assertions. But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms, likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct. If we're balancing a bank's accounts, I think we're safe. In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy. > This much math you need to know if you want to lecture others on the Internet. My original objection was completely appropriate to its context.
- catnaroek 11y ago
  > The system you outline works perfectly as long as you limit yourself to provable assertions. Of course. And if a formal system doesn't let you prove the theorems you want, you would just switch formal systems. > But Gödel's theorems have led to examples of unprovable assertions, thus moving beyond the hypothetical into a realm that might collide with future algorithms likely to be much more complex than typical modern algorithms, including some that may mistakenly be believed to be proven correct. Programming is applied logic, not religion. And a proof doesn't need to be “believed”, it just has to abide by the rules of a formal system. In some formal systems, like intensional type theory, verifying this is a matter of performing a syntactic check. > If we're balancing a bank's accounts, I think we're safe. I wouldn't be so sure. > In the future, when we start modeling the human brain's activities in code, this topic will likely seem less trivial, I see this as more of a problem for specification writers than programmers. Since I don't find myself writing specifications so often, this is basically Not My Problem (tm). Even if I wrote specifications for a living, I'm not dishonest or delusional enough to charge clients for doing something I actually can't do, like specifying a program that claims to be an accurate model of the human brain. > and the task of avoiding "arbitrary programs," and undecidable assertions (or even recognizing them in all cases), won't seem so easy. I don't see what's so hard about sticking to program structures (e.g., structural recursion) for which convenient proof principles exist (e.g., structural induction). Please, get yourself a little bit of mathematical education before posting your next reply. You're so stubbornly wrong it's painful to see.

deleted 11y ago

[deleted]

dllthomas 11y ago

> "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." You seem to be mixing up where the "for all" lies. The result is: There does not exist a procedure that, for all (program, input) pairs, the procedure will say whether the program halts for that input. {p | Ɐ(f,i): p(f,i) says whether f(i) will halt } = ∅ You are using it as if it said: For all (program, input) pairs, there does not exist a procedure that will say whether the program halts for that input. Ɐ(f,i): {p | p(f,i) says whether f(i) will halt } = ∅ "post evidence (as I have done)" What is at issue is your incorrect assertions about what your evidence says. We read it, it contradicts you, everyone points this out, and you just ignore it and get louder.

lutusp 11y ago
> You seem to be mixing up where the "for all" lies. Not at all. My original objection was to the claim that a program could be proven correct, without any qualifiers. Any program, not all programs. As stated, it's a false claim. Your detailed comparison doesn't apply to my objection, which is to an unqualified claim. > everyone points this out ... Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing. > you just ignore it and get louder. I wonder if you know how to have a discussion like this, in which there are only ideas, no personalities, and no place for ad hominem arguments?
- dllthomas 11y ago
  > My original objection was to the claim that a program could be proven correct, without any qualifiers. Any program, not all programs. Let's be precise. Let P be the set of all programs. Let C(s) ⊂ P be the set of programs correct relative to specification s. As I read the original statement, it was saying, {p ∈ C(s) | p, s ⊢ p ∈ C(s)} is large enough to be useful I am not sure whether you read it differently. > As stated, it's a false claim. You have said this repeatedly, but all you have done in support of it is point at the Halting problem. The Halting problem says: ∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts)) You have claimed this eliminates the possibility of proving correct any non-trivial program: > [T]he Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct." I see no way to read that but as a claim that: (∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → p is trivial) Please supply a proof. Note that it's quite true that (∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → *s* is trivial) proved usually by reducing s to "halts" for any non-trivial s. > Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing. I am not deciding it by poll. I am pointing out that there are objections to your reasoning that you have not addressed and persist in not addressing - despite them being made abundantly clear, repeatedly. > I wonder if you know how to have a discussion like this, in which there are only ideas, no personalities, and no place for ad hominem arguments? You're accusing me, as a person, of not understanding that a discussion like this has no place for accusations against a person? My complaint was not about you as a person, but about the form of your arguments in this discussion.

geofft 11y ago

> In your next post, rise to the occasion and post evidence (as I have done) instead of opinion, or don't post. I have already done so. Did you read my comment about existential vs. universal quantifiers? Can you respond to it? This was the original claim: > It's false -- the Turing Halting problem (https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem) demonstrates that one cannot establish that a non-trivial program is "provably correct." This is the statement you quoted from Wikipedia: > Quote: "Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist." Do you agree or disagree that the quantifiers in these two statements are different? Do you agree or disagree that "the Turing Halting problem demonstrates that one cannot establish that every single non-trivial program is either 'provably correct' or 'provably incorrect'" is a different claim than the one originally made?