Re: No Go To's Forever!

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

Martin Dowie <martin@dowie-cs.demon.co.uk> writes:

> one of the reasons I had always been told for avoiding using gotos, was
> that it makes a program unprovable. a) was this true; 

No.

> and if so, b) is this still true?

No.  (Why should it have changed, BTW?  I wouldn't call something
unprovable unless it has been proven to be unprovable.)

One of the standard textbooks in computer science uses gotos quite
heavily, and it contains correctness proofs.  Although the proofs are
not "formal", and neither is the algorithm description, they are more
substantial than the "formal" proofs which I've seen at the local
CS department.

BTW: What does "formal program verification" mean in practice?
I was told that it must involve quantifiers and other fancy stuff.
Is this true, or are rigid, but non-formal proofs considered sufficient
(i.e. proofs whose formalization is easy, but tedious work, and which
would result in proofs nobody could understand).  After attending some CS
courses, I should probably know it, but our formal program verification
exercises where quite a nightmare (for example, we should prove the
correctness of an implementation without having the specification).