[SIGCIS-Members] Correctness and verification

Sat Jul 4 15:16:13 PDT 2020

Hi Matt:

Thomas Haigh’s pair of messages do an excellent job of outlining and describing some of a large body of computer science literature relevant to Matt’s question. However, the topics he covers, such as software errors, formal methods, correctness proofs, etc., can themselves be seen as part of a more general study, called dependability or trustworthiness, which provides a conceptual basis and body of knowledge for considering and dealing also with such all too real possibilities as inadequate or absent specifications, incomplete or erroneous “proofs”, whether of software or hardware. Some references:

Schneider, Fred B.,  (Ed.).  Trust in Cyberspace: Report of the Committee on Information Systems Trustworthiness, Computer Science and Telecommunications Board, Commission on Physical Sciences, Mathematics, and Applications, National Research Council, Washington, D.C., National Academy Press (1999) 332 pp. [Full text available at: http://www.nap.edu/readingroom/books/trust/]

Cofta, Piotr. Trust, Complexity and Control, John Wiley (2007) 310 pp. [ISBN 0470061308]

and if I may be permitted:

Avizienis, A., Laprie, J.-C., Randell, B. and Landwehr, C. Basic Concepts and Taxonomy of Dependable and Secure Computing, IEEE Transactions on Dependable and Secure Computing, vol. 1, no. 1, (2004) pp.11-33. 

Cheers

Brian Randell

> On 4 Jul 2020, at 18:58, thomas.haigh at gmail.com wrote:
> 
> Returning for part II of the answer, on actual bugs. 
>  
> There is a huge computer science literature relevant to Matt’s question, but the key words are “correctness,” “formal methods,” “specification language” and “verification” rather than “error” or “bug.”
>  
> With the Pentium bug, IIRC some bogus value in a lookup table deep in the processor caused it to give wrong answers. That’s an example of a situation where a finished system doesn’t perform in line with requirements. But how are requirements expressed? Typically with a written specification that leaves many things ambiguous. Going back to the 1950s a lot of work in systems analysis was aimed at coming up with methods to get specifications right so that the systems built from them would do what was required. 
>  
> A problem in the final system might be a result of a mistake in specification or in implementation. The computer science answer to this was to express specifications completely and unambiguously in mathematical terms and then prove that the final software/hardware would always do what the specification said. Both tasks were enormously difficult. A lot of the history is told in MacKenzie, Donald.Mechanizing Proof. Cambridge, MA: MIT Press, 2001 which is an extremely good book full of very clear explanations of difficult topics. This history includes the intervention of a philosopher, J.H. Fetzer, who IIRC said that claiming to prove any correspondence between a mathematical specification and a material object is a category error. So I’m sure there are pointers there to follow up for more recent philosophical work on the topic.
>  
> I gave some autobiographically grounded thoughts on some of this in a recent paper “Assembling a Prehistory for Formal Methods” which also points to some papers by Niklaus Wirth and Cliff Jones giving insider views on the history. http://www.tomandmaria.com/Tom/Writing/FormalMethodsHistoryPreprint.pdf My suggestion is that the formal methods movement was in large part an outgrowth of the original impetus and core community behind both the Algol effort and the 1968 Software Engineering Conference (which has less than generally suggested to do with what was offered under the banner of “Software Engineering” by the 1980s). That appeared in special issue on the history of formal methods, which includes other, more technical, items of possible interest: https://link.springer.com/journal/165/31/6.
>  
> Editing the Turing Award website (particularly ongoing work to add video clips to profiles) has also reminded me that several awards were given for work in this area, and in particular that the “model checking” approach has had a huge impact on how chip designs are tested. So Matt might want to look at the following entries:
>  
> https://amturing.acm.org/award_winners/hoare_4622167.cfm
> https://amturing.acm.org/award_winners/sifakis_1701095.cfm
> https://amturing.acm.org/award_winners/emerson_1671460.cfm
> https://amturing.acm.org/award_winners/clarke_1167964.cfm
>  
> Best wishes,
>  
> Tom
>  
>  
> From: Members <members-bounces at lists.sigcis.org> On Behalf Of Matthew Kirschenbaum
> Sent: Friday, July 3, 2020 12:55 PM
> To: members <members at sigcis.org>
> Subject: [SIGCIS-Members] the nature of computational error
>  
> Hello all,
>  
> I am interested in a better understanding of the nature of computational error. My sense is that actual, literal (mathematical) mistakes in modern computers are quite rare; the notorious Pentium bug of the early 1990s is the exception that proves the rule. Most bugs are, rather, code proceeding to a perfectly correct logical outcome that just so happens to be inimical or intractable to the user and/or other dependent elements of the system. The Y2K "bug," for instance, was actually code executing in ways that were entirely internally self-consistent, however much havoc the code would wreak (or was expected to wreak).
>  
> Can anyone recommend reading that will help me formulate such thoughts with greater confidence and accuracy? Or serve as a corrective? I'd like to read something fundamental and even philosophical about, as my subject line has it, the nature of computational error. I'd also be interested in collecting other instances comparable to the Pentium bug--bugs that were actual flaws and mistakes hardwired at the deepest levels of a system.
>  
> Thank you-- Matt
>  
> 
> -- 
> Matthew Kirschenbaum
> Professor of English and Digital Studies
> Director, Graduate Certificate in Digital Studies
> Printer's Devil, BookLab
> University of Maryland
> mgk at umd.edu
> _______________________________________________
> This email is relayed from members at sigcis.org, the email discussion list of SHOT SIGCIS. Opinions expressed here are those of the member posting and are not reviewed, edited, or endorsed by SIGCIS. The list archives are at http://lists.sigcis.org/pipermail/members-sigcis.org/ and you can change your subscription options at http://lists.sigcis.org/listinfo.cgi/members-sigcis.org

—

School of Computing, Newcastle University, 1 Science Square, 
Newcastle upon Tyne, NE4 5TG
EMAIL = Brian.Randell at ncl.ac.uk   PHONE = +44 191 208 7923
URL = http://www.ncl.ac.uk/computing/people/profile/brianrandell.html