Re: Python from Wise Guy's Viewpoint

From: Matthias Blume (find_at_my.address.elsewhere)
Date: 10/24/03 

Date: 24 Oct 2003 16:12:43 -0500

Ray Blaak <rAYblaaK@STRIPCAPStelus.net> writes:

> Matthias Blume <find@my.address.elsewhere> writes:
> > The following: The only way that the above could be false is that two
> > conditions are met:
> >
> > - Joe writes a correct program.
> > - There is no proof for the correctness> of that program (in the sense
> > of "there is no such proof now and it is not possible for anyone
> > to produce such a proof in the future").
> >
> > I find this extremely unlikely because I believe that Joe already had
> > the sketch of the proof in his head when he wrote his correct program.
> > That sketch could be made into a full proof (by fleshing it out and
> > possibly by correcting a few non-fatal problems that it might have).
>
> This is the heart of "our" disagreement with you. The sketch of the proof
> (which is necessarily informal) could NOT necessarily be made into a full
> proof.

Indeed, we have to agree to disagree here. A proof (however informal)
can be called a proof only if -- at least in principle -- it could be
formalized.

> The sketch of the proof could (should) be readily fleshed out enough to
> convince another human being of the correctness. The sketch of the proof might
> often in principle be able to be developed into a formal proof.
>
> It is just that it cannot be certain that you *always* can do it. In fact it
> is usually really really difficult to do it at all, just because of the
> tediousness of doing everything formally.

I don't dispute the fact that it is exceedingly difficult.

> People's reasoning steps are not restricted formal logic. People's
> talents are in fact at glossing over the details. Formal methods, on
> the other hand, are precisely about verifying all of the details,
> which is what makes them so difficult.

Sure. But if the humans claim to prove things informally even though
there is no formal proof for them, then this is nothing more than
black magic. I don't believe in black magic. If there is an informal
proof that deserves the name, then thery is also a formal one.

> Note also, that "there is no proof for the correctness" should instead be
> stated as "it is not known if there is a proof for the correctness".

No, no, no! I was specifically talking about the existence of proofs,
not whether or not we know about that existence.

To state my belief one last time succinctly:

Conjecture:

   If a human writes a correct (in some formal sense) program that has
   a practical purpose (**), then there is a (formal) proof of
   correctness (in the same formal sense of "correct") for that
   program.

(**) Without this disclaimer one could easily disprove this conjecture
as follows: Systematically write down *all* programs. Among them
there will be correct programs (infinitely many, in fact) for which
there is no correctness proof. qed.

By the way, it is impossible to give a counterexample to the above
conjecture. Proof: A counterexample, by definition, is some program
which we can prove to be both correct and impossible to prove correct.
Unless you can (non-constructively) show the existence of a
counterexample some other way, you cannot disprove the conjecture.
(The most obvious non-constructive way of showing the existence of a
counterexample I avoided with that (**) condition.)

Needless to say, I cannot *prove* the conjecture either, so I guess it
will forever have to be that: a conjecture.

Matthias

Relevant Pages

  • Re: Strategy for revolutionizing math and physics
    ... The orbit of Mercury is observed to be 87.969 days. ... far from the sun where the pointwise probability of existence ... mathematics, but conjecture. ... It is conjecture with respect to mathematics. ...
    (sci.physics)
  • Re: Strategy for revolutionizing math and physics
    ... far from the sun where the pointwise probability of existence ... Every point along the diameter of the Mercury's circular orbit is ... mathematics, but conjecture. ... It is conjecture with respect to mathematics. ...
    (sci.physics)
  • Re: goldbachs conjecture
    ... verifiability and falsifiability: ... Popper called the Goldbach Conjecture true if, ... when it comes on a counterexample. ... Popper's context of computational falsifiability) ...
    (sci.math)
  • Re: On limitations of the Mautsch Principle (was Re: ineqality)
    ... >>>Dave Rusin's ... >> A key requirement in my conjecture is that equality hold iff all ... >of the same homogeneity as P ... it's broken until I see an actual counterexample. ...
    (sci.math)
  • Re: Turing vs. Godel (Newbie Question) (A simple example)
    ... Turing shows that for any Turing machine M, ... the counterexample depends on M. ... Goldbach's conjecture. ... It halts if and only if the ...
    (sci.math)