Gérard Huet programming with Gilles Kahn at IRIA's bâtiment 8 in 1978.

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.