DOI 10.1007/s00165-012-0226-7 BCS © 2012 Formal Aspects of Computing (2012) 24: 305–306

Formal Aspects of Computing

John McCarthy (1927–2011) Cliff B. Jones

On October 24th last year Computing Science lost one of its most distinguished founding figures. Numerous obituaries have appeared and they show the breadth of John McCarthy’s contribution: he is variously acknowledged as the “father of AI” or the inventor of Lisp. This short note1 acknowledges the huge debt that the area of “formal methods” owes to John. There is of course a clear link with John’s contributions to both AI and programming languages. Theorem proving was an early challenge for AI researchers (see [McC59, McC62, McC63b, McC65]). Lisp [McC60] is not everyone’s favourite programming language but few would deny the huge influence of ALGOL 60[BBG+ 63]: John was an influential member of that uncharacteristically successful IFIP committee. The real debt to John McCarthy becomes clear when one (re-)reads [McC60] which includes: Primarily, we would like to be able to prove that given procedures solve given problems . . . Instead of debugging a program, one should prove that it meets its specification, and this proof should be checked by a computer program. For this to be possible, formal systems are required in which it is easy to write proofs.

A clear and oft-quoted call is contained in [McC63a] (first presented at the May 1961 Western Joint Computer Conference) It is reasonable to hope that the relationship between computation and mathematical logic will be as fruitful in the next century as that between analysis and physics in the last. The development of this relationship demands a concern for both applications and for mathematical elegance.

Bear in mind that this was before the crucial contributions from Bob Floyd and Tony Hoare. This paper also addressed the question of the appropriate logic for reasoning about expressions that can fail to denote values. The use of logical operators defined by conditional definitions has some inconvenient properties but has been followed by, among others, David Gries and Fred Schneider and the RAISE specification language.2 Not only did John McCarthy recognise the need to reason about programs, he also made clear the importance of compiler correctness. On the first aspect, his focus was more on reasoning about recursive functions than the imperative programs but the (difficult) concept of “recursion induction” was an important tool and [McC63b] explores the link between recursive functions and ‘Algolic Programs’. At the 1964 Baden-bei-Wien IFIP Working Conference, John [McC66] introduced the idea of defining languages by abstract interpreters. This view of operational semantics was a major influence—not least on the work of the IBM Lab Vienna’s huge undertaking to provide an operational semantics for the PL/I language. Another influential development was the compiler proof based on operational semantics [MP66].

Correspondence and offprint requests to: C. B. Jones, E-mail: [email protected]. 1 Formal Aspects has been fortunate to publish some excellent balanced obituaries but on this occasion we were unsuccessful in contacting the right person in time —this note is offered as a substitute because the editors did not feel they could let McCarthy’s passing go unacknowledged. 2 In checking [McC63a], I note that there is an early proof of rev (rev (s))  s. Another of his challenge problems was the proof of the “91 function”.

306

C. B. Jones

I remember it as a privilege to have met John on a number of occasions and, if the reader will forgive the indulgence, some of these memories show interesting aspects of his character. The first meeting was on a visit to Stanford in the mid 1960s; I was honoured to be offered a lift to his AI lab by so great a figure but this feeling was quickly overtaken by, let us say, “unease” at John’s driving style behind the wheel of a Mustang. This was not our only contact that connected with cars: at the November 1967 meeting at IBM Yorktown, I had my first contact with snow chains. As a thaw set in, I was instructed by John in their removal. Far more important though were some of the technical insights from that meeting. The work of David Luckham, David Park and Mike Paterson on program schemata [LPP70] was provoking a lot of interest and Mike Paterson spoke on his just-completed thesis [Pat67]. John was far more excited about the new work of Zohar Manna and urged everyone to forget schemata and focus on the assertion based ideas in [Man68, MM69]. I mentioned the kindnesses that John showed to put in contrast the fact that he could express his displeasure very strongly and openly. At another event, an IBM speaker was incautious enough to hint that there was related research that he couldn’t talk about because it was company confidential. John was to give the after-dinner speech and clearly had prepared notes but after a few minutes put these aside and delivered a withering attack on companies that expected to benefit from science without sharing all of their own research. Anyone in the audience from IBM—and that included me— was left feeling profoundly uneasy. McCarthy continued to work on programming languages and I only learnt from his web page that he returned to his work on “Elephant” [the language that never forgot (values)] again after his nominal retirement from Stanford in 2001. The last time I met John was when we were together on a panel discussion at MFPS in April 2004. When invited to cross the Atlantic to take part in a panel, I was about to decline—until the organisers told me the names of the other panelists. The event was recorded and would have been worth preserving—sadly the sound is barely audible but I can still hear in my mind that characteristic start to a comment from John “Well, let me see . . . ”. To fill in the many gaps in my one-sided account, the reader is urged to look at http://www-formal.stanford. edu/jmc/ which characteristically omits to mention his Turing Award in 1971 or the fact that he was honoured with the Kyoto prize in 1988.

References [BBG+ 63] [LPP70] [Man68] [McC59] [McC60] [McC62] [McC63a] [McC63b] [McC65] [McC66] [MM69] [MP66] [Pat67] [Ste66]

Backus JW, Bauer FL, Green J, Katz C, McCarthy J, Naur P, Perlis AJ, Rutishauser H, Samelson K, Vauquois B, Wegstein JH, van Wijngaarden A, Woodger M (1963) Revised report on the algorithmic language Algol 60. Commun ACM 6(1):1–17 Luckham DC, Park DMR, Paterson MS (1970) On formalised computer programs. J Comput Sys Sci 4:220–249 Manna Z (1968) Termination of Algorithms. PhD thesis, Carnegie-Mellon University McCarthy J (1959) Programs with common sense. Mechanization of thought processes, vol. I. Her Majesty’s Stationery office, London McCarthy J (1960) Recursive functions of symbolic expressions and their computation by machine, part I. Commun ACM 3(4):184–195 McCarthy J (1962) Computer programs for checking mathematical proofs. In: Proceedings of Symposia in pure mathematics, vol 5. American Mathematical Society, New York, pp 219–227 McCarthy J (1963) A basis for a mathematical theory for computation. In: Braffort P, Hirschberg D (eds) Computer programming and formal systems. North-Holland Publishing Company, pp 33–70 (A slightly extended and corrected version of a talk given at the May 1961 Western Joint Computer Conference) McCarthy J (1963) Towards a mathematical science of computation. In: Popplewell CM (ed) Information processing’62. North-Holland Publishing Company, New York, pp 21–28 McCarthy J (1965) A proof-checker for predicate calculus. Stanford Artificial Intelligence Project Memo 27. Computer Science Department, Stanford University McCarthy J (1966) A formal description of a subset of ALGOL. In: [Ste66], pp 1–12 Manna Z, McCarthy J (1969) Properties of programs and partial function logic. In: Meltzer B, Michie D (eds) Machine intelligence, vol 5. Edinburgh University Press, Edinburgh, pp 27–37 McCarthy J, Painter J (1966) Correctness of a compiler for arithmetic expressions. Technical Report CS38. Computer Science Department, Stanford University (see also (1967) Mathematical Aspects of Computer Science. In: Proceedings of Symposia in applied mathematics, vol 19. American Mathematical Society, New York, pp 33–41). Paterson MS (1967) Equivalence problems in a model of computation. PhD thesis, University of Cambridge Steel TB (1966) Formal language description languages for computer programming. North-Holland Publishing Company, New York

Published online 17 April 2012