Trusting computers through trusting humans: software verification in a safety-critical information system

This article considers the question of how we may trust automatically generated program code. The codewalkthroughs and inspections of software engineering mimic the ways that mathematicians go about assuringthemselves that a mathematical proof is true. Mathematicians have difficulty accepting a computergenerated proof because they cannot go through the social processes of trusting its construction. Similarly,those involved in accepting a proof of a computer system or computer generated code cannot go throughtheir traditional processes of trust. The process of software verification is bound up in software qualityassurance procedures, which are themselves subject to commercial pressures. Quality standards, includingmilitary standards, have procedures for human trust designed into them. An action research case study ofan avionics system within a military aircraft company illustrates these points, where the software qualityassurance (SQA) procedures were incommensurable with the use of automatically generated code