Re: Python from Wise Guy's Viewpoint

From: Erann Gat (spammers_must_die_at_jpl.nasa.gov)
Date: 10/24/03 

Date: Thu, 23 Oct 2003 17:37:29 -0700

In article <m165ifobqz.fsf@tti5.uchicago.edu>, Matthias Blume
<find@my.address.elsewhere> wrote:

> The only time no formal proof can be given *in principle* is when
> there, in fact, is no proof. If there is no proof, we cannot know
> whether the program is correct. I don't consider programs for which I
> cannot know whether they are correct (even in principle!) useful.

I doubt that very much. You're posting to usenet, which means you are
making use of a significant software infrastructure, which means that you
ipso facto find it useful. I doubt very much that you could prove the
software infrastructure correct. (I doubt very much that it *is*
correct.) I am absolutely certain that you do not know that it is
correct, and that you never will. I am also quite certain that you will
continue to use it (and therefore judge it useful) regardless.

> Now, the programmer might think he has a proof but, in fact, does not.
> In that case the attempt of formalizing it would fail -- something
> that would be relatively easy to detect. So human errors
> notwithstanding, programmers do reason about their code, and that
> reasoning COULD be used to either verify correctness or to reject
> program, reasoning, or both on the basis of the fact that the
> reasoning was illogical.

Yes, but the only way to know whether or not this is possible in principle
is to actually do it in practice. There are no non-constructive proofs of
the existence of a proof.

> > To which my reply will be: how do you know that the exhibited proof
> > is correct?
>
> Because I checked it.

How do you know that you didn't make a mistake when you checked it?

> > Oh, you're going to run an automatic proof checker on
> > it? How do you know that the proof checker is correct?
> > How do you
> > know that the hardware on which your proof checker runs is correct?
> > What happens if you get a single-event upset in a processor
> > register, or a bad byte of RAM?
>
> What is the probability of this falsely giving a "proof ok" rather
> than a core dump?

First, what difference does that make? I thought you were arguing for the
desirability of proofs in an absolute sense, not a probabilistic one. If
you are arguing probabilistically then we have to compare apples and
apples and ask how much effort you have to put into a proof to gain a
certain confidence in its correctness and compare that to how much effort
you have to put into empirical testing to gain the same level of
correctness.

Second, I'll bet you that even a "proven" correct program would not
produce the expected results when run on a Pentium with the fdiv bug.

> Sure, there has to be a "trusted computing base" just like every logic
> has a set of axioms which we don't question any further. The point is
> that the trusted computing base can be small: proof checkers are
> fairly simple programs,

But they run on very complicated hardware. And they are compiled by very
complicated compilers, at least if you want them to run fast.

> I did not say "formal proof in their head", please! I said that the
> proof in their head ought to be formalizable, which is something
> entirely different.

I do not see it as entirely different. The only way to know if a proof in
someone's head is formalizable is to formalize it. Maybe they don't need
to do this in their head, but they do have to do it. Otherwise you're
just blowing smoke.

> You are right, btw, in that the discussion is becoming increasingly
> vacuous. Let's forget about the "I would fire her" remark, ok?

Fine.

> What
> I really meant to express with that remark was my belief that every
> programm actually *does* have a proof of correctness for her program
> in her head. Otherwise what she is doing amounts to randomly cranking
> out code without any understanding at all. A monkey at the keyboard.

There is a whole branch of research in evolutionary programming that uses
precisely that technique. In fact, some biologists are starting to look
at biological systems in computational terms. No one proved your DNA
correct, but it seems to get the job done nonetheless.

> That this is not what's going on was precisely my point: people do
> reason about their code (albeit informally in most cases, and many of
> them wouldn't be able to clearly communicate their reasoning). That's
> why I think that -- in principle -- all programs that people write and
> that turn out to be actually correct are, in fact, provably correct.

And I'm saying that you're wrong. You are wrong when you say that this is
the case, and you are wrong when you say (or imply) that this ought to be
the case.

> Finding and writing down the formal proof in practice, however, is a
> different story.

Indeed. But unless one does write down the formal proof in practice, what
is the point? Is there any content in your position beyond simply saying
that all else being equal it is better to think clearly about a problem
than not? I'll agree with that, but it doesn't strike me as a
particularly noteworthy observation.

> > P.S. Suppose your task is to write a typesetting program and one of the
> > requirements is that the output look aesthetically pleasing. How would
> > you go about proving that your code is correct?
>
> Obviously, this task is not well-defined

It is perfectly well defined, it's just defined in terms that are not
logical but rather psychological. There are people who make their living
(indeed an entire industry devoted to) solving this problem. You will
obviously not be among them.

E.

Relevant Pages

  • Re: Help with a problem
    ... >> If one's aim is to use nd to formalize the inferences of informal ... The reasoning from "If r is positive, ... This is described as an elegant and simple derivation by Keith ... Informal proof: ...
    (sci.logic)
  • Re: Torkel Franzen on truth
    ... things and are convinced about their arguments without even know what ZFC ... Axioms and rules of inference are connected only to *formal* reasoning. ... The point is that even if you could be able to formalize the ...
    (sci.logic)
  • Re: 9 Handed vs. 10 Handed Tables
    ... Just off the top of my head: ... Your BEST odds, if I understand your reasoning, would be in heads up. ... The reason one plays at 9-10 seat tables is that with more opponents, ... But the heads-up game is a lot more dependent on psychology: ...
    (rec.gambling.poker)
  • Re: More on Function Purity
    ... his program (because it simplifies this reasoning). ... replace expressions like head (head getArgs) with 'p'. ...
    (comp.lang.functional)
  • Re: Ranking from multiple columns
    ... In my follow-up just now, I forgot to discuss that I ... on its head for them. ... I explained my reasoning in a different ... Dallman Ross ...
    (microsoft.public.excel.misc)
Loading