FOM: Re: Re: Re: Godel, f.o.m.

[Steve Stevenson]

charles silver writes:
 > I guess a more direct question is to ask whether people think that the
 > formal approach to program verification is of value at all, given the many
 > kinds of errors that can creep in.  Are the benefits of program verification
 > outweighed by its weaknesses and costs?  Or, given that you have a certain
 > amount of money to spend for assuring program correctness, would the money
 > be better spent looking for other test mechanisms than for formal
 > verifications?

Actually, that's a sorta loaded question, even though you didn't mean
for it to be :-)

I'm no expert in verification. I continue to be interested in
verification ideas because, if taken in the right light, they may well 
lead us to interesting ideas.

In the short term, we will improve the tools and they may well become
reliable enough to use in every day programming in conjunction with a
period of testing. The last phrase ... in conjunction... I add to
recognize the *engineering* aspect of developing computer
systems. Nancy Leveson gave a talk where she used the following (much
abbreviated account):

	Big aircraft firm uses software that was supposed to have 
	one catastrophic defect in 10^16 seconds. On the first
	landing approach, it failed. Before taking the controls, the
	test pilot shook his watch and said, "10^16 seconds
	already. My, how time flies."

Anything that helps make computing more reliable is worth doing, IMHO. So my 
answer is that in the short term, we should continue to improve and we 
should continue to look in new directions. I'm a hard core, Errett
Bishop finitist; I get the feeling that I'm pretty much alone with a
bunch of platonists. I don't think your favorite, first order language 
with first order nonlogical axioms is the way to go. Strictly my
view. I'll listen to others ....

With regards to costs, I think it must be taken with the risks. For
example, a 1200 line code verified for a Canadian reactor cost many
millions of dollars to do. With a reactor, maybe the cost is justified 
based on the risk. The nuclear weapons codes, probably.

In the long run, the outlook is much more interesting. Being an old
compiler man, I know how little we understand about the language
side. Theories about the pragmatics of programming languages are ---
and should be --- formal but we don't use them much in real
compiling. It is hard to reason without clear formal statements about
what a language does *that is enforced and verifiable in any compiler
for that language*. Until we can do that, my own feelings are that it
is interesting but not usable. How bad is this: In Les Hatton's
article cited below, he shows experimentally that simulations lose
one order of magnitude accuracy for every change of
computer/compiler. That's unacceptable. 

steve



@Article{hatton97,
  author = 	 {Les Hatton},
  title = 	 {The {T} Experiments: Errors in Scientific Software},
  journal = 	 {IEEE Computational Science and Engineering},
  year = 	 1997,
  month =	 {Apr-Jun},
  pages =	 {27--38}
}