Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!cs.utexas.edu!asuvax!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1881@optima.cs.arizona.edu>
Date: 14 Apr 91 21:31:38 GMT
Sender: news@cs.arizona.edu
Lines: 79

In article  <1991Apr11.214018.19443@watmath.waterloo.edu> Michael Coffin writes:
]I assume you mean that proofs are a just a form of redundancy---a way
]to "write the program twice".

More than just writing the program twice, you also write the program
in a different style -- hopefully leading to different kinds of
mistakes.

]...  Programming languages, at least imperative
]languages, are constructed from statements, which say "do this, then
]this, etc.".  They don't say "achieve this goal", which is really the
]purpose of running a program.

Proofs don't say "achieve this goal" either.  They say "if the
preconditions are such, then then post conditions are such".  It isn't
clear to me that this is closer to the original idea.

]Here's an analogy to illustrate the difference (off the top of my
]head, so let's not push this too far).  Suppose I'm telling you how to
]get to my house.  A strictly imperative program looks like

I'll take the analogy with the caveat that the person following the
directions will make no mistakes.  It is the directions that might be
in error...

]Proving a program is like adding landmarks to the program and then
]showing that the actions get from one landmark to the next:

How is adding landmarks different from redundancy?

]Besides giving you more confidence while you're driving, the proof has
]the property that it abstracts away detail.

I don't believe that.  The amount of detail you have to specify is
dependent on the data structures you have available and to some extent
on how well the paradigm matches the problem.  It is not true that the
paradigm of predicate logic requires less details in general than the
paradigm of imperative procedures.

]In the original
]program, it's difficult to see if "go straight 4.1 miles" is right
]without trying the entire route; there's no mention of what "go
]straight 4.1 miles" ought to *do*. That's all informally
](mis)understood.  In the proven program, that statement can be checked
]in isolation...

I don't believe that either.  The effects of any procedure are as
formally understood as predicate logic.  How do you know what 3 < 4
means?  At some level all formalism is defined informally, and I don't
see why this is any less legitimate for programming languages than it
is for logic.  Also, it is not true that you can't see if "go straight
4.1 miles" is correct without trying the entire route.  You know
unambiguously what the effect of an instruction is given any
particular start state.

My gripe is that you _know_ what effect "x := 3" has.  It doesn't give
any better level of understanding to write "{true} x := 3 {x = 3}".
All you are doing is defining one notation in terms of another.  You
can also define predicate logic in terms of another notation, so that
instead of writing "x = 3" you would write "x = 3 |- <x,3> elem S".
At what point do you stop defining one notation in terms of another?
(For logicians out there: yes, this notation stacking has some uses,
but program verification is not one of them.)

]...  For concurrent
]programs, where nondeterminism can cause a program to run for weeks
]and then suddenly fail, I would guess that proofs are far more
]reliable. 

It may be that there are as yet no adequate testing methods for
parallel programming in procedural languags.  It may also be that
predicate logic is a more convenient paradigm for parallel programming
than imperative procedures.  But that is a seperate question from the
one of whether formalism for its own sake give some sort of magical
verification advantages.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman