Re: pitfalls of verifying floating-point computations

[Nick Maclaren <nmm1@xxxxxxxxxxxxx>]

David Hough 754R work <754r@xxxxxxxxxxx> wrote:
> For formal methods, the ultimate yawning chasm is between the
> specification of the behavior of a large complex program that's in
> mind of the user/programmer/specifier, and the specification that
> the formal method understands.

Grrk.  No.  That is the first chasm.  There is another, equally wide
and deep, which is between what the formal method specifies and what
the implementation delivers.

> "Doesn't solve all problems" could be an objection to any of them, but
> fortunately "helps to solve some important problems" is good enough. 

Sometimes.  And it can be harmful, as I claim is the case here.

It is common for 90% of the effort/problems to occur in 10% of the
cases.  If an approach makes the simple problems 10% easier and the
hard ones 10% harder, then a politician's viewpoint is that it is
a winner.  But an engineer's one is that it is a loser.


Regards,
Nick Maclaren,
University of Cambridge Computing Service,
New Museums Site, Pembroke Street, Cambridge CB2 3QH, England.
Email:  nmm1@xxxxxxxxx
Tel.:  +44 1223 334761    Fax:  +44 1223 334679