Re: Problems with proofs

[cpp@netcom.com (Robin Rowe)]

To: srt@zaphod.csci.unt.edu (Steve Tate)
Sb: Re: What good is halting prob?

Steve,

<< 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!) >>

Geez, Steve, I thought you liked me. Time for a refresher on that 
Dale Carnegie course?

<< 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?

By the way, please define the term "formal" as you are using it 
here with regard to specifications.

<< 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.

<< Typically assertions in the code are used to guide an actual 
proof of the correctness of the actual code. Nothing else is useful. 
>>

I'm not clear what you are trying to say here. Are you actually 
saying that the only really useful proofs are those expressed in 
code? (I think so, too, but this is a radical viewpoint!)

<< Proofs of correctness must be machine verified to be accepted. 
>>

Please define the term "verified" as you are using it here.

<< 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?

<< I have no idea what you mean by random error. >>

Cosmic rays, accidents, etc.

<< [Proofs take into account hardware failure] if the spec includes 
this, and they don't if the spec does not. >>

Isn't this a pretty loose way to look at proof? Proving that you 
conformed to a (possibly erroneous) specification sounds a lot less 
impressive than saying you have a "proof of correctness." 

<< I think you have an idea that a program that is proved correct 
is guaranteed to work. >>

A mind reader you're not.

<< If you have a 100% track record in implementing code that 
exactly conforms to its specifications, wonderful! I think proof of 
correctness won't help, but if, like most people, you find that one 
of the many weak links on the chain is in incorrect implementation 
of specifications, then proof of correctness....>>

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.

Thanks for the feedback. Good points.

Robin

-- 
-----
Robin Rowe       cpp@netcom.com       408-626-6646          Carmel, CA 
Rowe Technology  C++ Design/Training  Email for sample C++ Newsletter!