4 ms·

> 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 qua

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

by lutusp 11y ago

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.