Boost logo

Boost :

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
>can easily reason about the exception-handling behavior of large systems.
>don't know if there is an analogue in the domain of concurrent
>but I think it is worth searching for.
>----- 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

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


Boost list run by bdawes at, gregod at, cpdaniel at, john at