When Logic Meets Engineering: Introduction to Logical Issues in the History and Philosophy of Computer Science

1. Preface

The birth, growth, stabilization and subsequent understanding of a new field of practical and theoretical enquiry is always a conceptual process including several typologies of events, phenomena and figures spanning often over a long historical period. This is especially true when the field in question is not uniquely identified by either the Academia, or the Laboratory, or the Industry. Computing is a paradigmatic case. So diverse and conflicting are its origins, that the debates on the nature of computer science have characterized its whole history. From its early beginnings onward, computing has been variously labelled as a technology, a science and as a form of mathematics. It has been said that computing is a discipline dealing with machines that compute (see Newel et al. 1967), with information processed by such machines (see Hartmanis and Lin 1992) or with the algorithms that direct the behaviour of such processes (see Knuth 1974). Today, when computers are so extensively present in our lives, one would expect that theoreticians and practitioners in the field of computing would have found, at least, some consensus on these questions. The opposite is true however and there is still much controversy on the mathematical, engineering and scientific qualifications pertaining to the discipline.¹ The aim of the present special issue is to investigate these tensions within computer science by focusing on some of the figures and questions at the core of its relation with logic.

Until recently, besides few historical and philosophical contributions,² not much attention was devoted to the complexity of this topic. One reason for this is that in order to study the historical and philosophical influence of formal methods in computer science, one should also engage with the technology: to understand in what sense, for instance, Post production systems have played a role in the history of compiler design, or how a formal system like Hoare logic is the basis of systems used today to reason about programs in terms of states of the store and the heap. The need of technical understanding to write a proper history of computer science was recently at the centre of a debate within the community of historians of computing. In the 2014 Kailath lecture at Stanford titled Let's not dumb down the history of computer science, Donald Knuth explained his regret for the so-called professionalization of the history of computing which has implied an increasing neglect of technical content for the sake of more socially, institutional-, politically and/or industry-oriented histories. This talk resulted in lively discussions and finally a short piece (Haigh 2015) in the Communications of the ACM. A similar argument holds for the philosophical community as well. Computing and engineering at large have always been a significant source of inspiration for philosophical research. Such research has been directed either to the conceptual analysis of important and largely appealing themes, for example incompleteness and complexity; or it has focused on non-technical, often ethically oriented topics. This has attracted some interest from computer science practitioners, who have indulged in technically aware reflections on their discipline, but a common field recognized by all parties, where philosophers dare to be really technically prepared is still missing.

Precisely to tackle such need for a history and philosophy of computing that engages with both formal and actual computational and programming practices, the first International Conference for the History and Philosophy of Computing (HaPoC) was organized in 2011 and was followed by the foundation of the DHST/DLMPS inter-divisional Commission for the History and Philosophy of Computing (HaPoC).³ One of the aims of the commission is to organize regular meetings, providing an open platform for historians, philosophers, computer scientists, logicians, programmers, mathematicians (and all other figures involved by the field at large) to discuss across their own disciplinary boundaries and to offer the open environment required to reflect on all facets of computing. The present collection of papers, which resulted from the first International Conference on the History and Philosophy of Computing and subsequent events, aims exactly at this kind of reflection, by bringing to the fore the problem of bridging the gap between formal methods and practices of computing.

2. The significance of logic within the history of computer science

With the rise of the modern computer and the practices that surrounded it, came the realization that modern computing is as much a product of engineering as it is the result of formal and mathematical science. For instance, as Stan Ulam, an important figure in early computing practices of the late 1940s and 1950s, recounted (Ulam 1980, p. 94):

It is perhaps a matter of chance, that computer development became possible only by a confluence of at least two entirely different streams. One is the purely theoretical study of formal systems. The study of how to formalize a description of natural phenomena or even of mathematical facts. […] The whole idea of proceeding by a given set of rules from a given set of axioms was studied successfully in this connection. The second stream is the technological development in electronics, which came at just the right time.

These two different aspects of computer science, moreover, are not strictly separated: logic and technology work together, from the lowest hardware level, governed by Boolean circuits and arithmetical operations in the stack memory; through the structure of assignment, sequencing, branching and iteration operations defining modern high-level programming languages; up to the equivalent abstract formulations of recursive definitions for algorithms. Accordingly, (the history of) computer science can be understood only by investigating the non-straightforward and nonlinearly proceeding interactions between logic and engineering practices, which influenced each other and which received, moreover, further stimuli from external areas such as developments in business or the experimental sciences.

The logical foundations of computing are, at least, well-known. They can be traced back to the extensively studied debate on the foundations of mathematics from the end of the nineteenth—early twentieth century. The Grundlagenkrisis in mathematics notoriously brought the three foundationalist approaches to the fore: the logicist, the formalist and the intuitionist programmes.⁴ The derivation of Russell's Paradox in Frege's Grundgesetze der Arithmetik, determined the collapse of the first of these programmes, which aimed at deriving all mathematics from purely logical notions. This drawback in the search for foundations meant that Hilbert's finitist and formalist programme was reinvigorated in its attack of problems such as consistency and decidability. It is within this context that the work by mathematicians such as Church, Kleene, Post and Turing has its origins. They each contributed in making the idea of calculation a central topic in logic, by proposing different formalizations of computability,⁵ effective calculability,⁶ generated set⁷ and solvability.⁸ These formalizations were in the spirit of the formalist programme, in the sense that they allow ‘to abstract from the meaning of the symbols and to regard the proving of theorems (of formal logic) as a game played with marks on paper according to a certain arbitrary set of rules’ (Church 1933, p. 842). Such formalizations were required to prove that there is in fact no finite method to solve Hilbert's Entscheidungsproblem, or other related decision problems. As such, these results, next to Gödel's incompleteness, broke Hilbert's dream of making mathematics void of ignorabimus.⁹ The fundamental problem of determining for any assertion of first-order calculus whether or not it is valid, Hilbert's Entscheidungsproblem (Decision Problem) in its original form, was proven (recursively) unsolvable by Church, who showed it depends on the recursive solvability of problems in the λ-calculus¹⁰ and by Turing who showed its dependence on the decidability of decision problems for Turing machines, most notably the problem which we know today as the halting problem.¹¹ Similar problems were also proven unsolvable by Post already in the early 1920s. Despite this strict link to effective calculability, the mere idea of using computations in (practices of) mathematics was very much opposed by Hilbert, who considered the practical concerns of calculation removed from his interests.¹² Ironically, it were exactly the different formalist devices and techniques by which impossibility results were obtained, such as the universal Turing machine or the λ-calculus, that would also allow to provide (some of) the theoretical foundations of computer science.¹³

The third foundationalist programme also had an important and lasting influence on the theoretical foundation of computing. Brouwer's subject-based constructivist interpretation of mathematical truths, resulting in the formalization of Intuitionistic Logic by Kolmogorov and Heyting in the early 1930s with the rejection of the Law of Excluded Middle, reflected more closely the algorithmic reconstruction of the rules for classical predicate logic. This approach matched the idea of execution of rules for a classical language. Later, the coupling of logic and computation was advanced further. The algorithmic operators of the combinatorial calculus were defined as computationally equivalent representations by trees of any operation in the (untyped) version of the λ-calculus (and hence to recursive functions). In this they constituted a further Turing complete language. The equivalence of the type of such operators to the axiom schemas and function application corresponding to Modus Ponens made this in turn equivalent to the implicational fragment of Intuitionistic Logic (and hence the typed λ-calculus), as suggested by Curry; this equivalence was later rediscovered by Howard for natural deduction, a correspondence known today as the Curry–Howard isomorphism, which influenced the construction of computational systems like Martin-Löf's Type Theory and (much later) the development of proof checkers and automated theorem provers, such as Coq and Isabelle/HOL. The family of strongly normalizing typed systems are today the basis for various functional programming languages, with guarantee of important properties such as termination (by strong normalization) and memory access consistency (by typing).

But the relevance of these formal results in logic for later computing practices was certainly not evident, if not entirely disregarded, in the early days: the modern computer was not developed yet and the original context of those formal works was pure rather than applied mathematics. In this latter context, human and machine computational practices became more and more important because of, amongst others, advances in military research, requiring for example new firing tables for every type of new gunnery.¹⁴ It is for instance well-known today that ENIAC, one of the first electronic and programmable computers, was the answer to the problems encountered at the Ballistic Research Lab at Aberdeen Proving Ground with the timely computation of ballistic tables: the combination of the computations of the differential analyzer—an analogue machine—and the teams of human computers could not cope with the demands of the military. They were too slow.¹⁵ It was within this context of slow, error-prone human and machine computations that the first electronic and programmable computers such as ENIAC, the Baby Manchester machine, the EDSAC or the ACE and EDVAC designs were developed in the late 1940s.¹⁶ These machines were real behemoths when compared to modern-day computers and access to them was restricted to a selected number of people with diverse backgrounds: engineers, like Eckert and Mauchly, but also mathematicians or logicians like Turing, von Neumann or Curry. Partly thanks to the war effort, these people were forced to work together and disciplinary boundaries had to be crossed, especially between pure mathematics and engineering. Before that time, the connection between logic and digital circuitry had been made, amongst others, by Claude Shannon and Victor Shestakov who showed how to represent digital circuits by Boolean algebras.¹⁷ Beyond this basic hardware level, though, the electronic programmable computer required a deeper reflection on the use of logic to control computations: on the one hand, programmability meant the possibility of use for a variety of purposes; on the other, the electronic nature of computers meant they were too fast for humans to follow the computation. As von Neumann explained (von Neumann 1948, p. 2):

[It is] necessary to consider carefully the ability of the computing mechanism to take our intention correctly. And the person controlling the machine must foresee where it can go astray, and prescribe in advance for all contingencies. To appreciate this, contemplate the prospect of locking twenty people for two years during which they would be steadily performing computations. And you must give them such explicit instructions at the time of incarceration that at the end of two years you could return and obtain the correct result for your lengthy problem! This dramatizes the necessity for high planning, foresight, and consideration of the logical nature of computation. This integration of logic in the problem is a consequence of the high speed.¹⁸

Computers were born from the need for speed and precision in computations; and now logic was called for controlling (the correctness of) computations that were too fast for humans to check. One application of this requirement is the so-called stored-program idea which, roughly speaking, meant storing both instructions and data in the machine.¹⁹ Another application was the development of the flowchart notation by von Neumann and Goldstine which relies heavily on logical terminology (for instance, the use of bound and free variables).

With the need for logical control over dynamically performed computations came also the need to develop communication means, feasible for both machine and human user. In the early days, such communications proceeded either through direct physical wiring (as in the case of the orginal ENIAC) or through a very primitive order code very close to the machine. As a result, ‘programming’ the machine, as we call it today, was an extremely laborious and error-prone task and it became clear that much time could be gained if one could communicate with the machine in a ‘language’ that would abstract more from the hardware and allow to automate processes, for example, calling a subroutine and returning to the main procedure.²⁰ Of course, this meant also the need for a computational method to ‘translate’ such language to machine language. In this way, the steady development of so-called high-level programming languages and compilers went hand-in-hand. The first compilers and languages were developed in the late 1950s. Logic kept playing a crucial role: to give a few examples, Haskell B. Curry, who had also worked with ENIAC, developed in the late 1940s a theory of program composition insisting on the significance of formal logic in this context;²¹ Chomsky relied on Post's formal devices to define his hierarchy of languages which even today forms the foundation of compiler design;²² McCarthy used notions coming from λ-calculus and recursive functions to define the LISP language.²³ Simplicity of programming and increasing computational power helped the commercialization of the computers, the emergence of the programmer's profession and the increasing academic acknowledgement of computer science.²⁴ These developments resulted in a range of problems which have been identified as a software crisis in the late 1960s and (especially) early 1970s by a selected group of people. Dijkstra, during his Turing award lecture in 1972, which had a profound impact on the community, used the term software crisis as follows (Dijkstra 1972, pp. 860–861, the italics is ours):²⁵

[In the early days] one often encountered the naive expectation that, once more powerful machines were available, programming would no longer be a problem, for then the struggle to push the machine to its limits would no longer be necessary and that was all that programming was about wasn't it? But in the next decades something completely different happened: more powerful machines became available, not just an order of magnitude more powerful, even several orders of magnitude more powerful. But instead of finding ourselves in a state of eternal bliss with all programming problems solved, we found ourselves up to our necks in the software crisis! […] The major cause is […] that the machines have become several orders of magnitude more powerful! To put it quite bluntly, as long as there were no machines, progamming was no problem at all; when we had a few weak computers, programming became a mild problem, and now we have gigantic computers, programming has become an equally gigantic problem.[…] To put it in another way: as the power of available machines grew by a factor of more than a thousand, society's ambition to apply these machines grew in proportion, and it was the poor programmer who found his job in this exploded field of tension between ends and means.

Typical problems that started arising were software failure, unreliability and malfunctioning, at least partly due to large software projects becoming too complex to manage. These problems were considered by some the result of the theory lagging behind the demands and expectations of society, a reflection which led to the development of a new discipline called software engineering. Software engineering at that time, with a slightly more confined meaning than today, was referring to the use of formal methods within programming as a means to attack typical problems of this so-called crisis. At the same time it was also aimed at providing a more scientific status that a part of the community aspired to ascribe to the discipline by developing a solid theoretical methodology. Figures of the calibre of Dijkstra and Hoare defended the programs-as-proofs identity, with criteria of correctness and termination being paramount and to be proven in a logical or mathematical fashion.²⁶ New techniques were developed to integrate more logical approaches into programming methods.²⁷ For example, Dijkstra's method of ‘structured programming’ was developed to deal with, amongst others, problems of correctness;²⁸ Scott and Strachey developed denotational semantics for programming;²⁹ and de Bruijn aimed at formally verifying the whole of mathematics by writing AUTOMATH, a language also making use of types to induce the identity of theorems and output of an automated derivation.³⁰ But while these researches pointed at the primal role of logic in the design and construction of programs, the essential and delicate balance between the theoretical and practical aspects pertaining to computing was becoming pressing. The introduction of, for instance, the typed lambda-calculus into computer science was meant as a faithful modelling of well-specified computations in formally correct expressions. But the former, when intended as calculations actually executed on finite machines, operated by fallible programmers and users in a given social context, exceed the degree of precision of the latter by a much higher level of complexity. This position, counter-balancing the formalist view on correctness and validation with a more practical approach, was soon put forward by part of the computer science community. The reference to the social and multi-layered aspect of computational well-functioning (see, e.g. De Millo et al. 1979), as well as the practical impossibility to exclude essential aspects of computational malfunctions due to the physical nature of the processes involved (see, e.g. Fetzer 1988) were considered.³¹

Despite tensions between those insisting on the role of logic and those less convinced of its applicability have been recurring throughout the history of computer science, the need for formal methods is higher than ever. One major reason, present already in the above quotes by von Neumann and Dijkstra, is that the more ambitious society becomes in applying computation, the lesser control we have over what is happening inside the (networks of) machines. As a result, automatic certification relying heavily on formal methods is becoming increasingly important, especially in the context of cyber-physical and safety-critical computational systems like in avionics and the autonomous automotive industries, that is, in applications where computations are no longer taken in isolation, but rather as elements in sensitive connection to humans.³² Hence, it is clear that the relations between formal logic, engineering practices and physical machinery characterize some fundamental issues within computer science and its history: tensions and convergences which one needs to reflect upon to understand the nature of the discipline.

3. Discussion of contributions

In the present special issue we approach various apparently distinct issues concerning computability at large, correctness, software design and implementation, program semantics and human–computer interaction, with each contribution being commonly characterized in a double way: first, each author plays with the combination of historical background and philosophical insight we consider essential in exploring a technical and theoretical relevant issue in computing; second, every contribution insists on the relevance of logic and formal methods as the counterpart to the engineering practice, constituting the double face of the discipline. The arrangement of the papers in this volume also reflects a historically aware presentation of facts and topics.

We have already briefly pointed out above how the most common lore, which traces the history of computing back to the role of Turing, is largely a simplification. The logical roots of computer science are to be contextualized in a larger set of research fields and figures, each contributing specific and very crucial results to the field as we know it today. Certainly Turing deserves a prominent position. As historians and history-aware philosophers of computing, however, it is of the greatest relevance to understand how, why and by whom Turing came to be recognized very often as the father of the discipline. This is the task that Edgar Daylight is set to approach: with a historical analysis that stretches over results in logic including not only Turing, but recasts of his results by Kleene, Rosenbloom, Markov, he is able to identify a particular group of actors—including Booth, Carr, Gill and Gorn—who were looking for a more theoretical foundation of computation and found it in (recast versions of) the work of Turing.

The two decades across the 1960s and the 1970s have been often identified as a turning point for the development of computing as an academic and scientific discipline: many of the research methods currently at its core were initiated at this time, both at the low-level of machines, the higher-level of programs and the communications between them. The software crisis and the problematic confrontation with implementations solicited the development of new programming paradigms and semantic theories of programming like the denotational, axiomatic and event-based ones, aimed at a mathematical theory independent from particular implementations and allowing, for instance, to prove program correctness or equivalence. The problems associated with connecting the formal approaches with the practice of computing became apparent also in this context. Maarten Bullynck reflects on the case of the computation of a list of primes to discuss stepwise, structured and formally verified programming and considers the limitations imposed by user-machine interaction in implementations for systems such as the MULTICS and the ILLIAC IV. In what could be seen as a parallel exploration of the limitations of logical approaches to the semantics of programs, Felice Cardone reconstructs the historical and conceptual evolution of the principle of continuity from recursion in the 1950s, through Scott's denotational semantics at the end of the 1960s and Dijkstra's work in the 1970s: in this formal analysis, continuity is identified and explained as the principle that qualifies performed computations as finitary, and hence bounded by the time-related constraints of mathematical computation to be executed by machines, a notion that will have large conceptual consequences in modern computing, for example, for concurrency.

The mentioned debate on the notion and theoretical possibility of formal verification is at the core of the duality between logic and engineering in computer science. In open contrast with practitioners like Dijkstra and Hoare who understood programs as instances of proofs and insisted on the need to prove their correctness by logical means, the highly debated and influential paper (Fetzer 1988) claimed the impossibility of such a request, in view of the physical, non-purely theoretical nature of computational objects. The debate on program verification has spanned for decades, and has never been really closed, still generating conflicts of ideas today. In his contribution, Selmer Bringsjord re-opens the debate at a different level, by attacking the very core of Fetzer's argument, namely its logical consistency, claiming it is a self-refuting position on the basis that it is construed on the very same fallibility that the original attributes to computing. Hence, once again, logical correctness and physical implementation of computation (in humans or in machines) are opposed and compared, in what seems to reinforce the dual nature of this field. This relation between the logic of the machine and the logic of the human is at the core of the analysis of the final contribution: Graham White explores—with the help of many historical examples—how the various levels of abstraction from hardware on, are controlled by languages that are meant to accommodate the human user's intention and her understanding of the computation to be performed, and how such relation moves also in the opposite direction, with improvements in hardware and software to force accommodations by the user.

With this collection we hope to strengthen the bridge between the community of historians and philosophers of logic with computing. It is essential that both areas better understand and appreciate how computing and the related machinery represent the evolving state of formal logic; and how the latter has been a crucial, although not unique element, in the evolution of the former.

Notes

1 See Tedre 2015 for a recent in-depth study of the past and ongoing debates on what computer science is.

2 See, for example, Mahoney 1988, Aspray 1990, MacKenzie 2001, Davis 2001, and Turner 2014.

3 The website of the commission can be found at www.hapoc.org. For a more detailed discussion of the need for more technical content within the history and philosophy of computing, see De Mol and Primiero 2014.

4 See, respectively, Carnap 1931, von Neumann 1931, and Heyting 1931 for a historical representation of these three programmes. For a collection of source texts on the foundations of mathematics, see van Heijnoort 1967.

5 See Turing 1936/37.

6 See Church 1936a.

7 See Post 1965. Post developed this notion and its formalization in terms of generated sets in 1921 and proved on its basis the (absolute) unsolvability of a particular decision problem for his normal systems. However, he did not submit the results to a journal. In 1941 he submitted an account of this work from the early 1920s to the American Journal of Mathematics. The paper was rejected but a shortened version was finally accepted and published in 1943.

8 See Post 1936. These notions of course expanded on iteration and recursion, whose first definitions can be traced back to Bolzano (unnoticed), Cauchy and Weierstrass. See Adams 2011 for an extensive but accessible historical recollection of the notion of recursion as the foundation of computability.

9 See Mancosu et al. 2009, p. 94, where it is explained that

[It was one of Hilbert's aims to provide] a mathematical justification for his belief that all well-posed mathematical problems are solvable [i.e. the non-existence of ignorabimus in mathematics] […]. This […] aim resulted in two specific convictions: that the axioms of mathematics, in particular, of number theory, are complete […] and secondly that the validities of first-order logic are decidable (the decision problem). Soon [after Gödel's incompleteness theorems] Church was able to show […] that the remaining aim of proving the decidability of predicate logic was likewise doomed to fail.

10 That is, his formalization of effective calculability (next to general recursive functions). More precisely, he proved that the problem to decide for any λ-defined formula whether or not it has a normal form is recursively unsolvable (Theorem XVIII of Church 1936a). On the basis of this result, Church was able to show that the Entscheidungsproblem is unsolvable in any system of symbolic logic which is adequate to a certain portion of arithmetic and is ω-consistent (as a Corollary of Theorem XIX in Church 1936a). In another short paper, Church 1936b, he then showed that this result can be extended to first-order logic, hence proving the unsolvability of Hilbert's Entscheidungsproblem.

11 More specifically, Turing proved that there exists no (Turing) machine which allows to decide for any Turing machine whether or not it is circular or circle-free. In Turing's terminology, circularity means that the machine never writes down more than a finite number of symbols (halting behaviour). A non-circular machine is a machine that never halts and keeps printing digits of some computable sequence of numbers. On its basis, Turing then proved that also the problem to determine for any given machine whether or not it will ever print some symbol x cannot be computed by a Turing machine and showed that this problem can be reduced to first-order logic. For a comparative study of the different formalizations proposed by Church, Kleene, Post and Turing and their connection with decision problems, see Gandy 1988.

12 In an influential report on algebraic number theory known as Zahlbericht and published in 1897, Hilbert explicitly favours a more conceptual approach over a computational one (see for instance Corry 2008 for more details).

13 See for instance the papers by Felice Cardone and Edgar Daylight in this volume.

14 In Polachek 1997, p. 25, the following description is given of firing tables:

[D]uring the Wold War II period [t]he Army depended entirely on the accurate aiming of shells our guns fired at enemy targets. […] The procedure was to aim first at enemy targets based on information provided in firing tables and, in the event the target was missed, to make corrections on information also provided by these tables […] The information in the table was used directly by the gunner or was incorporated in the firing mechanism appended at the artillery equipment, anti-aircraft gun, or bomb sight.

For a detailed study of calculatory practices before the rise of the modern computer, see Grier 2007.

15 See Grier 2007 and Polachek 1997.

16 There has been much debate within the history of computing about ‘the first’ computer. Today, historians consider this question no longer legitimate since much depends on how one defines ‘computer’ and adjectives such as ‘stored-program’ or ‘general-purpose’ which one often associates with it.

17 See Shannon 1938 and Shestakov 1941.

18 The italics is ours.

19 See Haigh et al. 2014 for a detailed discussion of the stored-program concept. This principle has led to attributing the invention of the modern computer to Turing, because his Universal Machine requires instructions to be treated as data and conversely. It is clear, though, from recent historical research, that the development of the idea of the electronic, general-purpose and stored-program computer is more complicated and cannot be attributed to Turing alone. See especially Daylight 2014 and Haigh 2014.

20 For a discussion of the introduction of the so-called language metaphor in computer science, see Nofre et al. 2014.

21 Amongst others, he connected this work to combinatory logic, lambda calculus and recursive functions. See De Mol et al. 2015 for a detailed discussion.

22 See, for example, Chomsky 1959.

23 See McCarthy 1960.

24 See for instance Ensmenger 2010.

25 The 1968 NATO Software Engineering conference is the classic reference for the origin of the term ‘software crisis’. As it has been argued in Haigh 2010, one should be careful in overestimating the impact of this so-called crisis and the NATO conference. In fact, as he shows, ‘the idea of a ‘software crisis’ entered common use […] following the 1972 Turing Award lecture […] [of] Edsger Dijkstra’ Haigh 2010, p. 3.

26 See for instance Dijkstra 1968 and Hoare 1969. The story and origin of the extended Curry–Howard isomorphism is still partly unclear and deserves an analysis on its own.

27 See the paper by Maarten Bullynck in this volume.

28 See Dijkstra 1972.

29 See Scott and Strachey 1971.

30 See De Bruijn 1968.

31 The complex formulation of notions of formal correctness, reliable design, effective debugging and so on are all still central issues in the academic and industrial development of mainframe and especially software systems. For a philosophical, rather than strictly technical, categorization and definition of the problem of computational errors, see, for example, Fresco and Primiero 2013 and Floridi et al. 2015. For the argument on the practical impossibility of program correctness, see for example the paper by Selmer Bringsjord in this volume. For the evolution of computational systems in relation to the user, see for example the paper by Graham White in this volume.

32 By way of example, consider the recent development of a formally verified C compiler, part of the CompCert project (see http://compcert.inria.fr/motivations.html):

[This compiler is not] [f]or non-critical, ‘everyday’ software [where] bugs introduced by the compiler are negligible compared to those already present in the source program [but for] safety-critical or mission-critical software, where human lives, critical infrastructures, or highly-sensitive information are at stake.