3 ms·

> "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 u

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

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.