GRAPA: more accessible proof assistants
Date :
Changed on 11/08/2023
Focused on the benefit of programmers, the French-Chilean team GRAPA (GRAdual Proof Assistants) has as its main goal to extend the scope of gradual typing to full type theories, to support fluent certified programming in a new generation of proof assistants.
In this Associate Team collaborate researchers from the Inria Centre at Rennes University and the Universidad de Chile. This time, we spoke with its coordinators, Nicolas Tabareau, lead researcher of the Gallinette project-team, and Éric Tanter, professor at the Department of Computer Science of the Faculty of Physical and Mathematical Sciences of the Universidad de Chile and researcher in the Pleiad group, to learn more about their collaborative work.
Could you introduce us to GRAPA?
Éric Tanter (ET): The GRAPA team is exploring how to make proof assistants more accessible to programmers by supporting a relaxation of statically imposed hard constraints by rechecking during reduction. This general technique called gradual typing has been studied for standard programming languages, but very little for full-fledged proof assistants based on Type Theory. We are concerned both with the theoretical underpinnings of the approach, as well as with a concrete realization in the Coq proof assistant, and with the evaluation of the approach on realistic case studies.
Nicolas Tabareau (NT): While certified programming with proof assistants is undoubtedly an extremely appealing and powerful approach towards the systematic construction of correct, robust and secure software systems, it suffers from a proportionally large complexity problem that prevents wide adoption beyond very specialized crowds. An intrinsic part of this problem is the absolute reliance on static checking, whose conservativeness can be frustrating for developers, fostering the impression that the tool gets in the way of actual progress in software system development. This is why dynamic languages such as Python and JavaScript are still favored by large parts of the industry.
What is a proof assistant?
In computer science, a proof assistant is a software that allows the verification of mathematical proofs, either theorems or mathematical assertions. Proof assistants aim at proving theorems and are also intended to correct computer programs.
Coq, the result of a 25-year project driven by Inria, has become a preeminent tool in this domain. Coq is a formal proof management system that provides a formal language for writing mathematical definitions, executable algorithms and theorems, along with an environment for the semi-interactive development of machine-checked proofs. Coq is free, open source software and recognized in France by the National Certification Center.
Discover Coq: https://coq.inria.fr/
Discover the partnership between the Agence Nationale de Sécurité des Systèmes Informatiques (ANSSI) and Coq:https://www.inria.fr/fr/inria-partenariat-anssi-logiciel-coq-certification
Dynamic languages are flexible and easily accessible, but do not provide any correctness guarantee by construction. The GRAPA associate team is concerned with the general possibility of combining static and dynamic approaches within the challenging environment of dependent type theories, thus supporting gradual certified programming.
A gradual approach allows programmers to enjoy the benefits of static and conservative reasoning to the extent they desire, deferring the remaining analysis to runtime. The main objective of the GRAPA team is therefore to extend the reach of gradual typing to full-fledged type theories in order to support smooth certified programming in a new generation of proof assistants.
How did GRAPA originate and how did you first start collaborating?
ET: Our research teams have been collaborating for over 10 years. We have had associate teams continuously since then. This is in itself a follow-up to my PhD thesis which was co-directed with the Université de Nantes in 2000-2004, and my collaboration with Nantes until Nicolas Tabareau joined Inria in 2009.
NT: When I joined Inria in 2009, Éric Tanter was already actively collaborating with researchers in Nantes on other subjects. We quickly managed to merge our different backgrounds to attack a new problem, at the frontier of proof assistants and mainstream programming languages.
©
© Inria / Photo M. Magnin
What are the specific areas of research of each of you? What scientific questions do you seek to answer or have already answered with the project?
ET: My lab, Pleiad, is studying various programming languages and software engineering, with a recent focus on type systems, program verification and semantics. Inria's Gallinette project-team, led by Nicolas Tabareau, is focused on advancing Type Theory in general and the Coq proof assistant in particular.
NT: By using the competence of the Pleiad and Gallinette team, we would like to see how techniques to get more flexible mainstream programming languages can be reused in the setting of proof assistants based on type theory, which are very peculiar programming languages, but still programming languages.
What are GRAPA's objectives?
ET: In addition to the theoretical contributions, we expect:
-
produce a practical implementation of a gradual proof assistant, probably as an extension of the Coq proof assistant;
-
getting to a production level implementation is probably too ambitious at this point, but at least we can make progress on a usable proof of concept, applicable to small to medium sized projects.
Titre
What are the specific applications GRAPA could have or has had?
Image
Verbatim
"A gradual proof assistant would allow programmers to smoothly evolve programs, strengthening specifications and proofs of such programs along the way as required by a project's specific goals and requirements at a given point in time. The gradual aspect is the one that will allow this incremental approach to certify programming."
Auteur
Poste
Professor, Department of Computer Science, Faculty of Physical and Mathematical Sciences, Universidad de Chile, Coordinator of the GRAPA associate team
Image
Verbatim
"We hope that providing a more incremental mechanism to certified programming will help proof assistants extend its popularity and go beyond the current level. Indeed, even if proof assistants like Coq are now very popular in some particular application areas, they are far from reaching the entire software industry."
Auteur
Poste
Lead researcher of the Gallinette project-team, Inria, coordinator of the GRAPA associate team.
How does the work between the French and Chilean teams complement each other?
ET: I have been working on gradual typing in programming languages for more than a decade, and Tabareau is an expert in type theory and proof assistants. Therefore, the GRAPA project really exploits this synergy between both lines of expertise.
¿What is an Associate Team?
An associate team is a joint research project between an Inria project-team and a foreign research team. For a period of 3 years, the partners jointly define a scientific objective, a research plan and a program of bilateral exchanges.
Since Inria's arrival in Chile in 2012, 29 French-Chilean research projects in different areas of digital sciences have been funded under this program by Inria.
Currently, there are nine Associate Teams working, in which researchers from Inria centers in France collaborate, such as the Inria Centre at the University of Bordeaux, Inria Centre at the University of Grenoble Alpes, Inria Centre at the University of Lille, Inria Lyon Centre, Inria Nancy - Grand Est Centre, Inria Paris Centre, Inria Centre at Rennes University, Inria Antenna at the University of Montpellier, Inria Saclay Centre, Inria Centre at Université Côte d’Azur; and Chilean institutions, such as Universidad de Chile, Pontificia Universidad Católica de Chile, Universidad del Bío Bío, Pontificia Universidad Católica de Valparaíso, Universidad Adolfo Ibáñez and Universidad de O'Higgins.
