Re: Problems with proofs

[dewar@cs.nyu.edu (Robert Dewar)]

><< I would guess Robin has not actually had experience in proving
>correctness of programs from his comments, since they seem more like
>guesses as to what might be involved in the process (if I am wrong
> Robin, correct me!) >>

You ascribed this to Steve, you are mixed up! It was me (Robert) who asked
this, but in fact this note makes the answer pretty clear. I am beginning
to understand your style. You make pronouncements on things you don't know
much about in an attempt to provoke people into explaining them to you! OK
I'm happy to play that game, once I understand it :-) :-) Anyway, please
be assured this has nothing to do with liking you or not liking you. I don't
even know you (for all I know you are a Turing test teletype doing a
truly brilliant job :-)

><< Nope [to that proofs are based on what appears relevant to a
>human being to prove], proofs are based on formal specifications of
>the task at hand. >>

>So, it's not human beings who decide what belongs in the formal
>specifications?

 Sure, at some level this is true, but once the specification is constructed,
 it is no longer subject to human interpretation, and this is exactly what
 we mean by a formal spec, one whose semantics are mathematically specified,
 by some appropriate formalism, e.g. a reasonably powerful example would be
 first order predicate theory plus set theory.

><< This [that there is no proof that the proof is equivalent to the
>code] is based on a misconception, a proof of correctness, if is is
>any use at all, must have a formal relationship to the code. >>
>
>Please define the term "formal" as you are using it here.

 Again formal means that we have a formal specification as described above
 of both the language in which we write, and of the problem, and the formal
 relationship between the two is a proof that the program conforms to the
 specification.

><< Proofs of correctness must be machine verified to be accepted. >>
>Please define the term "verified" as you are using it here.

 Proof verifiers are a very old technology, some early examples exist from
 the early 60's and maybe even late 50's. A proof verifier is simply a
 program (which had better be verified itself), that checks a proof to make
 sure that you have not goofed, i.e. it simulates a VERY accurate high school
 math teacher looking at your proofs on an exam. The technology of these
 verifiers has been studied for years, and there are many products both
 academic and commercial.

><< Interfaces to components are part of the axiomatic structure of
>proven components, and on one side you prove that a component
>properly handles uses that conform to its interface, and on the
>other, you prove that the use by a client conforms to this
>interface. >>
>
>This sounds reasonable, and what I expected, too. However, I'm told that
>valid input parameter ranges are often specified arbitrarily. Invalid
>input is the user's (engineer's) lookout. Have I been misinformed? Is it
>generally more comprehensive?

 Sometimes yes, sometimes no, obviously if you are interfacing to the
 external world, you may simply have to start with a set of hopefully
 correct axioms about the behavior of the external world (here is a good
 place to build in your empirical safety factors if your information is
 imperfect).

><< I have no idea what you mean by random error. >>
>Cosmic rays, accidents, etc.

 From a formal point of view, these are simply hardware errors. Mathematics
 does not care whether things have gone wrong because of acts of God, or
 because of manufacturing defects, leave that up to lawyers!

><< I think you have an idea that a program that is proved correct
>is guaranteed to work. >>
>A mind reader you're not.

 And still many of your comments seen disappointed that proof of correctness
 turns out only to be proof of conformance to (possibly incorrect)
 specifications.
 >Hmmm, I may have to change my mind about the utility of the halting
>problem. Implementing code that exactly conforms to its
>specifications sounds like the halting problem to me.

 I hope it is clear from my previous note that while it is trivially true
 that the conformance problem is equivalent to the halting problem, this is
 irrelevant. There is nothing that says that you can't prove that a given
 Turing machine halts, just that you can't do this in general. Similarly,
 we can't prove correctness in general, but we can do it in specific cases,
 which is what we are interested in. 

Robert (not Steve)
(some of your quotes were indeed not from me, I did not answer them!)