PhD in Computer Sciences in Cleveland and enters at IRIA
Invited Professeur at Carnegie Mellon
Directeur de recherche de classe exceptionnelle at Inria
European Association for Theoretical Computer Science Award
Reminiscences of a computer science researcher, 1967-2000
I learned how to program in 1966, as a student engineer at Sup'Aero (French National Higher Institute of Aeronautics and Space), in PAF on a CAB 500 computer, and in ALGOL on a CAE 510 computer. Programs were typed on punched tape produced by an enormous typewriter, the Flexowriter. The carriage return was pressed with caution, as the carriage risked taking your arm off if it was in the way. The tape produced was then fed into the machine's tape reader, being careful not to cut your hand on the tape, which was very sharp at high speeds. Programming was a risky activity!
In the summer of '67, I managed to do an internship at CEA-DAM (French Alternative Energies and Atomic Energy Commission - Military Applications Division); the biggest - and top-secret - computing centre in France, where only military engineers with official secret clearance worked. As interns were forbidden there, I got myself employed as a 'computer maintenance technician'. There I developed, in Fortran, visualisation software of 3D surfaces, in stereoscopy and with animation.
After my aeronautical engineering studies and my master's in computer science (from the 1st class of 1969!), I left for the United States, just as the DOD (Department of Defense) was installing its Arpanet network linking the main American universities, boasting state-of-the-art equipment (PDP-10). It was a time of extraordinary creativity, in particular in artificial intelligence within the LISP community. I was naturally fascinated by this discipline, which for me represented the challenge of the 21st century. However the abundance of crazy ideas and exaggerated affirmations led me to concentrate on a precise technical challenge - the automation of mathematical reasoning.
I first of all created PETER, a first-order logic automatic demonstrator with equality, for my MSc . I had tinkered with the Stanford LISP compiler using an assembly patch to make it retrieve keyboard interruptions, which enabled me to implement an interactive proof assistant. We were barely able to prove even very simple theorems of algebra, but we had overcome a first challenge. PETER was the 'spiritual son' of SAM, produced by a small private company, Applied Logic Corporation, in Princeton. They had received a federal grant, a progress report of which was archived in a warehouse to which my director of studies had access. He had passed it on to me and I was astounded: this mysterious private company was doing far better than all of the major universities on this very mathematical subject.
It was very difficult to explain to mathematicians the pertinence of such research in automatic demonstration by computer. It would have appeared to them that we were only solving small combinatorial logic and algebra puzzles, far removed from contemporary abstract mathematics. The company was lacking an essential layer: the design of a mathematical vernacular language enabling both an expression of the parametric structure of the formulations and the modular structure of the proofs. This core notion had been set out by the mathematician N.G de Bruijn at the end of the 1960s, with the Automath system. However this pioneering effort, based on a uniform functional notation (technically, a λ-calculus with dependent types), was only recognised outside very restricted circles in the 1990s.
At the time I had no ambition to become a researcher, I considered myself a trainee engineer. Case Western Reserve University had accepted me onto its PhD programme, by giving me an assistant position, and I was free to choose my subject. I did not think that automatic demonstration was a promising field with regard to its short-term applications, and I turned towards the issue of resource-sharing concurrent process management, a crucial problem for the multi-task systems that were now equipping modern computers - the age of the batch was over. At the time, theoretical computer science was developing the notion of program schemata, and that is how I came to read the paper "Parallel Program Schemata" by Karp and Miller. I did not find in it any material to model my problem; however my attention was drawn to an undecidability result, obtained by dipping into the Post correspondence problem, which I discovered on this occasion.
Some time later, trying to remotivate myself in automatic demonstrations, my advisor slipped me a Princeton thesis, on the resolution of the unification problem (finding the common instance of two formulae) in theory of types (more precisely, in higher-order logic using Church's simply typed λ-calculus to represent the terms of the logic). This problem was fundamental to the generalisation of the demonstrators based on the resolution principle to higher-order logic that enables the direct encoding of the group theory and express principles of recurrence. By curiosity, I read the thesis, and had to learn the basics of the λ-calculus theory by reading Curry and Feys, the only available source on the subject at the time. The thesis presented different scenarios of the problem, which it broke down into sub-problems. It claimed to get from these a unification algorithm, but there was no proof of convergence of the inferred recursions. After persevering for some time, I went back to thinking about other, more concrete, problems. And then, some weeks later, as I was arriving home - more precisely, just as my door lock opened - the proof of undecidability came to me like a bolt from the blue: the Post correspondence problem was a sub-case of unification, I could visualise the two terms as being aligned on a simple encoding of the words in flat terms.
Beyond the anecdote, the lesson to be learned is that you must read outside your research subject area, and not wear yourself out on an obsessive problem. My luck had been to read the paper on automata, to have by chance learned the Post result there, having put to one side the problem of unification - something I did not understand well. My subconscious did the rest, a psychological 'Eureka moment' had precipitated the network of neurones that set to work in order to make the connection, and the proof was hatched by suddenly appearing in my conscious in a visual form. The formal proof of the result was but an administrative formality.
All of a sudden, my status went from agile programmer to star researcher. I had solved a major open problem in mathematical logic. Better still, I had discredited a Princeton maths thesis claiming the contrary - my PhD was in the bag. The negative resolution of the conjecture was in fact the identification of the termination problem of a complete unificator-search semi- algorithm that could be interlaced with the proof-search problem. Moreover, I demonstrated a sequentiality condition enabling the search for non-redundant solutions, by parallelising unification queries in a set of constraints. As a result I obtained a semi-algorithm for proof in theory of types, and therefore a methodology to interactively develop machine-verified mathematics. Incidentally, this technique was developed later under the generic notion of constraint programming.
My PhD guaranteed, I contacted M.P. Schützenberger with a view to applying to (the recently-created) IRIA, where he was one of the first scientific directors. In 1969 I had attended his captivating C4 lectures, which had given me a taste for combinatorial algebra. He pointed me towards Maurice Nivat, who had just set up a team there on program schemata theory. That was how I was hired to Rocquencourt in August 1972.
In 'Bâtiment 8' (building 8), which included scientists that were mathematically very specialised (such as Philippe Flajolet, Bruno Courcelle, Jean Vuillemin or Jean-Jacques Lévy), Gilles Kahn and I decided to embark on the creation of software for the structured manipulation of programs, despite the meagre equipment and software resources available to us at the time. We spent a lot of time discussing the future tool, but a decisive initiative by Gilles got the project started properly. One morning, I found Gilles on his hands and knees in his office, cutting up a big print-out using scissors. He explained to me that it was Wirth's recursive-descent compiler for Pascal. Gilles was cutting the print-out exactly at the points where the compiler produced assembler code. We copied out the rest, by inserting construction commands for abstract syntax trees, and there you have it - Mentor was born. Gilles called it 'minimum effort programming', and in fact he had invented the pre-digital copy-paste.
One day Pr. Böhm, a grand master of λ-calculus, paid us a visit. As I was showing him my unification work, he told me about a paper by Knuth and Bendix on algebraic rewriting. In it I found something exciting to get my teeth into - the theory of rewriting - which kept me busy for several years. Jean-Marie Hullot, a brilliant student from Orsay, where I taught a DEA (postgraduate degree) in computer science, joined me in order to put the theory into practice. In 1980 I took extended leave from IRIA to spend a sabbatical year at the Stanford Research Institute, in a team where Bob Boyer, J. Moore and Bob Shostak were working. I negotiated guest status for Jean-Marie, who was totally free to work on his KB software without worrying too much about laboratory management issues. Jérôme Chailloux in person came to set up the VLISP-10 from the University of Vincennes on our PDP-10, we were fully autonomous. This was a very productive year, and I brought my contribution to rewriting to a close with a survey on the subject, drafted with Derek Oppen who was then a postdoc at Stanford.
When I returned to Rocquencourt, the situation had changed with the arrival of Multics. In addition, Bâtiment 8 was bubbling over with excitement, with the launch of the national project VLSI. A VAX 780 with UNIX became the kernel of a small, independent computing centre in Bâtiment 8.Jean-Marie Hullot in 1982.
Jérôme joined the lab, to develop The_Lisp there. Then Yves Devillers provided us with the Internet, and, indirectly, the whole of France benefited from it, when officially IP protocol was forbidden as it was in violation of the European telecoms standards! We would sometimes take liberties with technocratic rules…
I prudently remained on the fringes of the VLSI maelstrom, running the Formel project, a small team co-directed with Guy Cousineau who had come to spend a sabbatical year. The aim of the project was to create a mathematical proof assistant system integrating cutting-edge research in the theory of types and in functional programming. The first prototype was developed from a LISP base provided by the LCF proof system recently developed at the University of Edinburgh, our preferred partner. LCF (Logic for Computable Functions) enabled the development of proofs of functional programs in a logic adapted to the notions of denotational semantics, the dominant paradigm of calculus models at the time. Above all, it made it possible to macrogenerate compound proofs by programs called tactics in a typed functional language guaranteeing the correction of these proof schemata, called metalanguage (ML). ML was a language interpreted by the underlying implementation language, LISP. The ML programs were, as a result, very slow, which was tolerable for the application to proof tactics, but unacceptable for use as an implementation language. However ML was by far the best-defined programming language mathematically speaking, in fact it was a λ-calculus equipped with a system of polymorphic types, enabling reliable and modular programming without being detrimental to its power of expression (completeness in the Turing sense), thanks to a recursion operator.
The challenge was therefore to improve its performance, keeping the LISP base until the bootstrap with a real compiler. Gilles had provided me with the LCF sources that I had put on The_Lisp in the lab. I spent entire nights reading the sources of this software, which was very professionally written. The most interesting module was the ML compiler in LISP. It was the direct definition of the denotational semantics of ML written in LISP. The variables were compiled in access to the environment represented by a binary tree. In it I could recognise the generalisation to a tree-structure environment of the de Bruijn indices of these variables. This little gem was the work of Lockwood Morris. One night, I carried out a daft experiment. Instead of interpreting with the LISP eval function the S-expression from this translation, I ran the result of its compilation with the LISP compiler. Execution time was immediately reduced by a factor of 10. The forefather of Caml was born. In retrospect, I see myself as a mechanic tinkering with the carburettor of a Rolls-Royce with a view to turning it into a Ferrari. Often, the stroke of genius is simply doing something ordinary that stands out a mile.
A small community was built up around ML, firstly with Larry Paulson, from the University of Cambridge, and Guy Cousineau, professor at Paris 7. Then a whole wave of research emerged around the design of a standardised ML, using various translation ideas of abstract machine code closures. In 1983, in Edinburgh, Luca Cardelli had implemented on UNIX an effective ML running on a functional machine. David McQueen, who had worked with Rod Burstall on the HOPE language, enabling the calling of functions by filtering its arguments (a specific case in unification), joined the design effort of a new language: Standard ML. From our side, Guy Cousineau had implemented recursive types and call by filtering. His PhD student, Michel Mauny, had implemented an abstract machine CAM, based on the work by Pierre-Louis Curien on categorical combinators. An intense design activity took place, with an informal technical journal called ‘Polymorphism’ publishing the proposals. Nonetheless, there was neither consensus on the module system nor on the syntax, and towards 1985 two different languages emerged: Standard ML developed in Edinburgh, Cambridge and Bell Labs, and Caml at INRIA Rocquencourt, within the Formel project which had been joined by Ascander Suarez, Pierre Weis and Alain Laville.
We still had a demonstration activity from Jean-Marie Hullot's KB demonstrator, which was the only one at the time to process equational theories with commutative and associative operators necessary for polynomial manipulations. In his thesis François Fages had positively solved the problem of Stickel's associative-commutative modulo unification algorithm termination, and expanded on the notion of canonical inference in propositional calculus and predicate calculus. Philippe Le Chenadec had worked on providing constructive versions of the principal results of algebraic combinatorics using the formal calculus algorithms that we had developed. Finally, an extension to a notion of constructor of inductive algebraic theories made it possible to do proofs by recurrence of small functional programs.
This line of research had become a discipline in itself - Rewriting - and a host of new researchers threw themselves into the competition, like it was a gold rush, still without having a realistic view of the altogether limited applications of this technology. For me, the principal results were established, the algorithms implemented and tested, and we therefore disposed of a solid base for equational demonstrations, however these equational formalities did not suffice on their own to express the more advanced mathematical notions necessary for the development of certified mathematics. The overall logical framework had to be sufficiently expressive to allow for the interaction of a human mathematician through a well-adapted formalised mathematical vernacular. The modularity necessary for the verification of major mathematical developments brought to mind the analogy with the programming languages. Indeed, the project's two research fields - typed functional programming and the verification of formal proofs - were a single area. Just like strict software engineering, as our colleagues in Gothenburg were already maintaining.
In the 1980s, numerous upheavals had affected mathematical logic. First of all, the (typed) λ-calculus was recognised as being isomorphic to the structure of proofs in Gentzen's natural deduction. The germ of the idea is found in Curry, then Howard explained isomorphism in the case of first-order logic, against a background of general indifference. In Eindhoven, Nicklaus de Bruijn had built Automath on this principle, with the λ-calculus used both for expressing functional terms, 'à la' Church, and constructing the proofs of a higher-order logic. This pioneering effort had remained largely ignored. At the beginning of the 1980s, the number of specialists in λ-calculus could be counted on the fingers of both hands: the students of Corrado Böhm in Italy, those of Niklaus de Bruijn and Henk Barendregt in Holland, Christopher Wadsworth in Edinburgh and Jean-Jacques Lévy, our local specialist in Rocquencourt. The first awareness of an influence of this calculus in programming had been, in the 1970s, the development of denotational semantics around the work of Dana Scott, Gordon Plotkin, Gilles Kahn and Gérard Berry.Nicolaas de Bruijn in 1994.
Among the mathematicians, in Paris Jean-Yves Girard had solved an important open problem in mathematical logic: the coherence of higher-order logic. This came down to proving a termination result of a typed λ-calculus, where the types enabled a genericity of the programs to be expressed. In fact, these polymorphic types were the generalisation of the ML polymorphism. And then we discovered that Girard's System F was isomorphic to the polymorphic λ-calculus proposed as a programming language by John Reynolds! In 1983, Thierry Coquand, a brilliant young mathematician, came to do his thesis in our team, to work with me on the design of a proof assistant combining the dependent types ideas of Automath with those of the polymorphic λ-calculus. The design of the logical framework, and its metatheory, were carried out hand in hand with the implementation - in Caml, of course. In early 1985, Thierry Coquand defended his thesis on 'The Calculus of Constructions', establishing the coherence of the logic. In parallel, I was implementing an interactive proof verifier, by formulating the construction of proofs using a set of tactics seen as the elementary operations of an abstract machine - the 'Constructive Engine'. The use of ML as a programming language allowed me to publish verbatim this implementation as a 'literate programming' paper in the sense of Don Knuth. In effect, an ML program is essentially a succession of higher-order recursive definitions on initial algebrae, and can therefore claim - without shame - the status of mathematical development. In fact, programming is just doing more precise mathematics than usual!
The convergence between programming and proofs suggested all sorts of interactions. Logic could be used to embellish programs through assertions, and develop a correct program technology by construction, the proof verifier being seen as a software development environment. It was even possible to synthesise the program by extracting it from its logical 'gangue' using a proof of its existence. Mathematical libraries could be developed, and the underlying algorithms could be extracted from them. Conversely, we could assemble the best computer science algorithms, and through their composition establish more elegant and more abstract demonstrations of traditional mathematics. If the tool was scaled up, it would become the benchmark working toolkit for both mathematicians and software designers. The prospects were exciting, but we were still a long way off having developed the Coq workshop to the point where these applications would become realistic.
In fact, it is the development of programs as typable l -terms in System F that had initially motivated me to use polymorphic types as structures of algebraic data. We could define arithmetical functions, and even iterators on complex data structures, using very simple combinators. Very early on, I had implemented - on The_Lisp - an evaluator similar to the G-machine in order to run these algorithms. In reality, this methodology turned out to be fruitless, for Christine Paulin-Mohring will demonstrate in her thesis the non-canonicity of these encodings, and suggested in their place an extension of the Calculus of Constructions with primitive inductive types, inspired by the work of Per Martin-Löf, a Swedish logician who led the research of the Gothenburg group, which had become our main partner. The ensuing logic system, the Calculus of Inductive Constructions, was finally adopted as a logical framework for Coq, which by then had been developed by new, young researchers doing their theses within the team, such as Gilles Dowek, Benjamin Werner, Hugo Herbelin and Jean-Christophe Filliâtre.
In 1985, a crisis arose in Bâtiment 8. The VLSI national project, which hosted our computational resources, notably VAX on which we carried out our developments, had to reduce its area of activity and asked its satellite projects, Algo and Formel to fly the nest. I took advantage of this to take a sabbatical year at Carnegie Mellon University, on the invitation of Dana Scott, taking four researchers and students with me. The course I developed there, which could be done in the 'literate programming' tradition, defined the state of the art in 'Formal structures for computation and deduction'. Upon our return to Rocquencourt, we had a usable prototype of a proof assistant for the calculus of constructions. The theory of types was beginning to be a major paradigm in programming research, particularly in Europe. Our resource issues were solved by the European programme ESPRIT, which funded, in our field, two 'Basic research actions' each for three years - 'Logical Frameworks' then 'Types'. These networks, coordinated by our Rocquencourt site, linked up the main groups working on the theory of types, in Gothenburg, Edinburgh, Cambridge, Utrecht/Eindhoven/Nijmegen and Turin. Along with Gilles Kahn's team, now in Sophia Antipolis, that redirected its Centaur effort towards PCoq, a human-computer interaction for proof assistants.
During this time, the part of the team developing Caml had attracted some brilliant young scientists who transformed the ageing Caml platform into an autonomous and efficient programming environment. Xavier Leroy implemented Zinc, then Caml-light, equipped with an optimised native code compiler, and an effective memory allocation backend thanks to Damien Doligez. Xavier then designed and implemented an elegant parametric module system, allowing separated compilation. Didier Rémy and Jérôme Vouillon added an object layer, and OCaml was born. It would prove itself to deserve its motto 'The language of choice for the discriminating hacker'.
The Formel team had now reached its maximum size, requiring the mitosis into two targeted team on two complementary niches: functional programming and theory of types. The first, Cristal, brought together the Ocaml effort, the second, Coq, focused on the proof aspect around the demonstration assistant, with the aim now of developing decision procedures enabling the automation of routine reasoning, such as the simplification of algebraic identities. We had come full circle, with automatic demonstration now buried in black boxes and the mathematician at the centre of the game, managing the assembly of theories. The pertinence of the approach was demonstrated in full scale, firstly in the Maths Components project led by Georges Gonthier at the MSR-Inria joint centre, with the formal proof of the four-colour theorem. Then, later, with Xavier Leroy's Compcert project, resulting in the formal certification of an optimising C compiler. These two ‘tours de force’ demonstrate that a robust technology has emerged from this research, and the increasing need for software with a high level of security guarantees the durability of these efforts.
This little history of the emergence of proof engineering with a strategic interest, from very speculative research on the bases of mathematics, provides a concrete illustration of the pertinence of Inria's R&D model. First of all, the facts mentioned in my journey are primarily the result of teamwork. I have named only some students and colleagues, however many others have made a significant contribution. The notion of a project team makes it possible to form commando groups with well-targeted goals and their limited duration, tempered by the protected status of public sector employee, enables the renewal of research themes and to avoid becoming stuck in the mud with methodologies based on fashionable phenomena, but which reveal themselves to be of little relevance in practice. Inria's recruitment policy of excellence makes it possible to attract the best scientists, trained by the French mathematics school. They turn towards our team in order to carry out their thesis work, because senior researchers are encouraged to teach at university and in higher education institutions and engineering schools, where they recruit their students. The encouragement to carry out theoretical research hand in hand leading to the publication and effective implementation of prototypes enables the concrete validation of the notions, and, potentially, the development of robust software over the long term: both Ocaml and Coq have required thirty years of development following the first prototypes. Finally, open source software has allowed us to, in effect, benefit from considerable leverage thanks to the international researcher community sharing not only its ideas, but also its software creations. Both Ocaml and Coq are the result of efforts such as LCF, themselves relying on the developments of the LISP community - their roots go back to the origin of the university-libertarian computer science of the 1960s.