Hacker News new | past | comments | ask | show | jobs | submit login

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




Join us for AI Startup School this June 16-17 in San Francisco!

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: