Proof and the computer: some issues raised by the formal verification of computer systems
Formal verification is the attempt to give a mathematical proof that the design of a computer system is a correct implementation of its specification. This effort raises questions about what ‘proof’ is. Two main conceptions — formal proof and rigorous argument — are identified, and it is suggested that they are underpinned by the disciplinary authorities, respectively, of logic and mathematics. The views of specialists in formal verification about the degree of certainty that can be claimed for verification are examined, and it is argued that the temptations to claims of certainty unwittingly offered by the commercial and regulatory environment must be resisted Copyright , Beech Tree Publishing.
Year of publication: |
1996
|
---|---|
Authors: | MacKenzie, Donald |
Published in: |
Science and Public Policy. - Oxford University Press, ISSN 0302-3427. - Vol. 23.1996, 1, p. 45-53
|
Publisher: |
Oxford University Press |
Saved in:
Saved in favorites
Similar items by person
-
Chains of finance : how investment management is shaped
Arjaliès, Diane-Laure, (2017)
-
Histoire des techniques et sociologie de la connaissance
MacKenzie, Donald A., (1998)
-
An engine, not a camera : how financial models shape markets
MacKenzie, Donald A., (2006)
- More ...