From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,86fd56abf3579c34 X-Google-Attributes: gid103376,public X-Google-Thread: 10db24,77f71d0bde4c5bb4 X-Google-Attributes: gid10db24,public From: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: Problems with proofs Date: 1995/04/20 Message-ID: X-Deja-AN: 101283302 references: <3kaksj$iur@isnews.calpoly.edu> organization: Courant Institute of Mathematical Sciences newsgroups: comp.lang.ada,comp.edu Date: 1995-04-20T00:00:00+00:00 List-Id: ><< 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!)