&gt; My original objection was to the claim that a program could be proven correct, without any qualifiers. Any program, not all programs.<p>Let&#x27;s be precise.<p><pre><code>    Let P be the set of all programs.

    Let C(s) ⊂ P be the set of programs correct relative to specification s.
</code></pre>
As I read the original statement, it was saying,<p><pre><code>    {p ∈ C(s) | p, s ⊢ p ∈ C(s)} is large enough to be useful
</code></pre>
I am not sure whether you read it differently.<p>&gt; As stated, it&#x27;s a false claim.<p>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><pre><code>    ∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))  
</code></pre>
You have claimed this eliminates the possibility of proving correct <i>any</i> non-trivial program:<p>&gt; [T]he Turing Halting problem (<a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Halting_problem" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Halting_problem</a>) demonstrates that one cannot establish that a non-trivial program is &quot;provably correct.&quot;<p>I see no way to read that but as a claim that:<p><pre><code>    (∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → p is trivial)
</code></pre>
Please supply a proof.<p>Note that it&#x27;s quite true that<p><pre><code>    (∃p ∈ P s.t. ¬(p ⊢ p ∈ C(halts)) ∧ ¬(p ⊢ p ∉ C(halts))) → ((p,s ⊢ p ∈ C(s)) → *s* is trivial)
</code></pre>
proved usually by reducing s to &quot;halts&quot; for any non-trivial s.<p>&gt; Again, this is a logical error. Science is not a popularity contest, and in this specific context, straw polls resolve nothing.<p>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.<p>&gt; 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?<p>You&#x27;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.