Re: No Go To's Forever!

[Florian Weimer <fw@deneb.cygnus.argh.org>]

Robert Dewar <robert_dewar@my-deja.com> writes:

> >Why should it have changed, BTW?
> 
> Becauswe proof of correctness techniques have improved!

Well, I thought that "unprovable" and "difficult to prove" mean
different things.  But you are the native speaker, and I won't argue
with you. ;)

> > and neither is the algorithm description, they are more
> > substantial than the "formal" proofs which I've seen at the
> > local CS department.
> 
> I have no idea what substantial means in this respect, 

The "formal" proofs I was shown had severe gaps, which could have been
filled, but doing so would have made them incomprehensible (at least
for me, the only thing which I could do with such proofs is checking
step by step whether they are valid, but I'm sure I couldn't learn
anything about proof techniques or the structure of the underlying
problem from them).

> > (i.e. proofs whose formalization is easy, but tedious work,
> > and which would result in proofs nobody could understand).
> 
> It is not really important if a human can understand a proof,
> if all proof obligations have been satisfied algorithmicly
> using a verifier.

That's the point.  I didn't know that such tools are available.  If
you use them, formal proofs suddenly make much more sense.