Abstract
The first part of this paper discusses floating-point arithmetic, as performed by computers and advanced digital calculators. It shows that different computer arithmetics have been proposed, and that the nearest approximation to a consensual computer arithmetic — the Institute of Electrical and Electronics Engineers' standard for floating-point arithmetic — had to be negotiated, rather than deduced from existing human arithmetic. The second part of the paper discusses mathematical proof of the correctness of programs and hardware designs, which is increasingly being demanded for systems crucial to safety or security. It argues that this extension of the domain of application of mathematical proof involves the negotiation of what a proof consists in. In 1987, this argument led the author and colleagues to predict a legal case concerning the nature of mathematical proof. Such litigation took place in 1991; the key point at issue is described. More general disagreement about proof as applied to computer systems is also discussed. A further prediction is made: that there will be litigation concerning not just what kind of argument counts as a proof, but over the internal structure of formal proofs.
Get full access to this article
View all access options for this article.