From: Beman Dawes (beman_at_[hidden])
Date: 2000-08-25 10:33:04
David Abrahams wrote:
>Maybe you and I have something different in mind. When I say "informal" I
>don't mean "unrigorous" in any way. A formal correctness proof has been
>shown to impracticable even for small programs without concurrency.
>
>I am thinking, for example, about the power of the basic/strong/no-throw
>exception-safety distinctions, and how with those three simple concepts
you
>can easily reason about the exception-handling behavior of large systems.
I
>don't know if there is an analogue in the domain of concurrent
programming,
>but I think it is worth searching for.
>
>-Dave
>
>----- Original Message -----
>From: "Bill Rutiser" <wru_at_[hidden]>
>> Let me add a warning about informal reasoning about concurrent
>> processes. There exist clever, efficient, synchronization schemes,
>> proved to be correct for two processes, that fail badly for three.
>>
>> -- Bill Rutiser
Hoare himself addressed this issue in a 1996 paper "How did software get so
reliable without proof?" There's an extended abstract at
http://users.comlab.ox.ac.uk/tony.hoare/icse18.html
Quoting the abstract, "...the techniques employed to achieve reliability
are little different from those which have proved effective in all other
branches of modern engineering: rigorous planning of procedures for design
inspection and review; raised levels of machine support for design
automation; quality assurance based on a wide range of targeted tests;
careful structuring of the product into modules and layers; continuous
evolution by adaptation of products already in widespread use; relaxation
of resource constraints and deliberate over-engineering (otherwise known as
defensive programming or belt-and-braces). Formal methods and proof play no
greater role in largescale programming than they do in any other branch of
modern engineering."
In other words, the same point that Dave makes: "informal" doesn't mean
"unrigorous".
--Beman