Merci d'avoir accepté l'interview
Version française
Peux-tu nous dire quelques mots sur ta thèse ?
Un langage de programmation nous permet d'exprimer de façon aisée comment doit agir une machine de sorte à accomplir une certaine tâche, qui peut être simple, tel comme l'addition des deux nombres ; ou plus compliquée, tel comme le calcul de la suite des nombres premiers. L'ensemble d'instructions qui est donné à la machine est ce qu'on appelle un programme. Un langage de programmation est alors un langage avec laquelle on peut parler aux machines et un programme est un morceau de texte qui une machine peut comprendre. Dans le sous domaine de l'Informatique fondamentale appelé Langages de Programmation, on cherche à étudier ces langages et les programmes pouvant ainsi être écrits. Cela nous amène à une question centrale : quel langage devrions-nous utiliser quand on veut parler des programmes ? Le lecteur pensera, peut-être immédiatement, au Français ou à l'Anglais, même parce que je l'ai déjà fait dans ce paragraphe en disant qu'un programme accomplit "le calcul de la suite des nombres premiers". Malheureusement, des langages naturels sont insuffisantes pour parler des programmes, car elles sont souvent imprécises laissant ainsi beaucoup d'espace à l'ambiguïté : lorsqu'on parle de la suite des nombres premiers, parlons-nous d'une suite infinie, ou d'une suite bornée ? Doivent ces nombres être produits d'un coup ou selon le besoin d'un deuxième programme qui demande le calcul de cette suite ? Pour répondre de manière satisfaisante à la question de comment parler des programmes de façon précise, des chercheurs à la fin des années 60 ont développé ce qu'on appelle les Logiques de Programmes : des langages permettant d'exprimer avec rigueur mathématique ce que fait un programme. Au début, cette méthodologie était limitée à des programmes simples comprenant des fonctionnalités tel comme l'écriture en mémoire ou l'itération d'une instruction en boucle. Une longue ligne de recherche s'est développée pour montrer que cette approche s'étend à des programmes bien plus compliqués.
Mon travail de thèse se trouve dans cette ligne de recherche. Plus spécifiquement, je m'intéresse à étendre la portée des Logiques de Programmes aux programmes avec des effect handlers. Les effect handlers sont une récente et puissante fonctionnalité de programmation. Souvent en programmation il y est nécessaire d'arrêter un programme de façon atypique car, par exemple, les données sont corrompues. Les effect handlers sont une généralisation de ce mécanisme : ils nous permettent d'arrêter un programme et aussi de le reprendre plus tard selon besoin. Ils ne sont plus alors restreints aux situations atypiques ou d'erreurs ; ils constituent une fonctionnalité en soit permettant l'implémentation de divers primitives et modes de programmation. Pour donner un exemple, avec les effect handlers, il est possible de programmer facilement avec des tâches asynchrones, c'est-à-dire, des taches s'accomplissant partiellement en même temps. Lorsqu'une de ces tâches termine, celles qui ont été interrompues en attendant son résultat peuvent être reprises. La figure accompagnant le texte montre encore une autre application des handlers, le calcul des nombre premiers, l'idée étant que lorsqu'un préfixe des nombres premiers a été déjà calculé, le programme peut être interrompu jusqu'à ce que le calcul du prochain premier soit nécessaire.
Les effect handlers posent un défi aux Logiques de Programmes, car, dans l'absence de cette fonctionnalité, un programme peut être vu comme une boîte noire qui reçoit des données et en produit de nouvelles. Les logiques de programmes usuelles reposent sur cette abstraction pour faciliter la description d'un programme : il suffit de décrire la relation entre entrée et sortie. Un programme avec les effect handlers par contre peut interagir avec son milieu à travers son interruption et reprise intermédiaires. L'idée clef dans ma thèse a été d'introduire la notion d'un protocole, qui décrit justement cette interaction. Dans mon manuscrit de thèse, je montre comment cette idée s'applique à divers exemples des programmes avec des effect handlers.
Peux-tu nous décrire ton parcours ?
J'ai commencé mon parcours académique au Brésil, où j'ai fréquenté l'Instituto de Tecnologia Aeronáutica (ITA), l'équivalent d'une école d'ingénieur, pendant deux ans. J'ai ensuite décidé de venir en France pour intégrer l'École polytechnique, qui était connue parmi les étudiants brésiliens de l'ITA comme une destination pour ceux qui cherchent une formation avec des fondements scientifiques plus rigoureux ainsi qu'une expérience à l'étranger. J'ai toujours aimé les sciences (en particulier les mathématiques et la physique), mais c'est en France que j'ai considéré l'idée de poursuivre une carrière académique. À la fin de la quatrième année de l'X, j'ai fait un stage de recherche au Computer Laboratory à Cambridge. J'ai travaillé avec un logiciel appelé Isabelle, développé originalement par Lawrence Paulson. Ce logiciel nous permet de rédiger une preuve mathématique de façon que chaque étape de raisonnement soit vérifiée obtenant ainsi une preuve sans faute. Cela a été une expérience très stimulante et qui m'a donné la certitude d'approfondir encore plus dans mes études. Je suis revenu alors en France pour un master à l'Université Paris Cité. Pendant le master j'ai eu la chance de faire encore un autre stage de recherche. Cette fois je l'ai fait avec François Pottier au sein de l'équipe Gallium (maintenant devenu Cambium) au centre Inria de Paris. J'étais très satisfait avec les résultats obtenus pendant ce stage et aussi très content avec l'orientation de François, c'est ainsi que j'ai décidé alors de poursuivre une thèse sous sa direction.
Quel a été ton parcours après la thèse? Quel poste occupes-tu aujourd'hui?
Après ma thèse, je suis venu à Londres pour travailler en tant que chercheur postdoctoral au sein du groupe dirigée par Azalea Raad à l'Imperial College. Je travaille sur un sujet assez diffèrent de ce que j'ai fait en thèse me permettant ainsi d'élargir ma compréhension du domaine. En particulier, je fais de la recherche sur les modèles de mémoire faible. Lorsque plusieurs tâches s'exécutent en même temps, ce qui est possible grâce aux processeurs dit à multi-coeur, il est tentant de vouloir expliquer ses possibles résultats comme s'ils étaient vénus d'un seul programme alternant entre ces différentes tâches. Cela n'est pourtant pas possible, car les processeurs réels comportent de manière beaucoup plus complexe à fin d'obtenir de l'efficacité. Le but des modèles de mémoire faible est justement de donner une description plus adéquate de ce qui peut faire des vrais processeurs.
English Version
Could you tell us about your thesis work in a few words?
A programming language allows one to express how a machine should work to perform a certain task, which can be simple, such as the addition of two numbers; or more complicated, such as the computation of the sequence of prime numbers. The resulting collection of instructions given to the machine is what we call a program. A programming language is thus a language in which we can talk to the machine and a program is a piece of text that a machine can read. In the subfield of Theoretical Computer Science called Programming Languages, we aim at studying these languages and the programs that can be so written. This goal takes us to a central question: which language should we use when talking about programs? The reader will think, perhaps immediately, about languages such as English, even because I have already within this very paragraph when saying that a program performs the “computation of the sequence of prime numbers”. Unfortunately, the English language is insufficient to talk about programs; English prose is often imprecise and ambiguous: when we talk about the sequence of prime numbers, do we talk about an infinite sequence, or a bounded one? Should these numbers be produced at once, or should they be produced according to the needs of a second program that asks for their computation? To give a satisfactory answer to the question of how to talk about programs in a precise fashion, researchers towards the end of the 60’s developed a method called Program Logics: languages that allows one to express with mathematical rigor what a program is supposed to do. At the beginning, this methodology was limited to simple programs including features such as writing to memory or iterating an instruction in a loop. Thenceforth, a long line of research has been developed showing that this approach extends to much more complicated programs.
My thesis work follows this direction. More specifically, I am interested in extending the scope of Program Logic to programs with effect handlers. Effect handlers are a new and powerful programming feature. In the exercise of programming, it is common that one needs to suddenly halt the execution of a program because, for example, the data is corrupted. Effect handlers are a generalization of such a mechanism: they let us not only interrupt a program but also resume it later if needed. They are no longer restricted to atypical or error situations; they constitute a functionality in themselves allowing the implementation of various primitives and programming modes. To give an example, with effect handlers, it is possible to easily program asynchronous tasks; that is, tasks that are executed at the same time but with the constraint that only one of these tasks can make progress at a time. Upon termination of such a task, those that were interrupted while waiting for its result can be resumed. The figure accompanying the text shows yet another application of handlers, the computation of prime numbers, the idea being that when a prefix of the prime numbers has already been computed, the program can be interrupted until the computation of the next prime is required;
Effect handlers pose a challenge to Program Logic because, in the absence of this functionality, a program can be seen as a black box that receives data and produces new data. Usual program logics rely on this abstraction to facilitate the description of a program: it is enough to describe the relationship between input and output. A program with effect handlers, on the other hand, can interact with its environment through its intermediate interruption and resumption. The key idea in my thesis was to introduce the notion of a protocol, which precisely describes this interaction. In my thesis manuscript, I show how this idea applies to various examples of programs with effect handlers.
Can you describe your journey to PhD?
I began my academic journey in Brazil, where I attended the Instituto de Tecnologia Aeronáutica (ITA) for two years. I then decided to go to France to join the École Polytechnique, which was known among Brazilian ITA students as a destination for those seeking a more rigorous scientific foundation as well as an experience abroad. I have always loved science (especially mathematics and physics), but it was in France that I considered the idea of pursuing an academic career. At the end of the fourth year of X, I did a research internship at the Computer Laboratory in Cambridge. I worked with a software called Isabelle, originally developed by Lawrence Paulson. This software allows us to write a mathematical proof so that each step of reasoning is verified, thus obtaining a faultless proof. It was a very stimulating experience and one that gave me the certainty to delve even further into my studies. I then returned to France for a master's degree at Université Paris Cité. During my master's degree, I had the chance to do yet another research internship. This time I did it with François Pottier within the Gallium team (now Cambium) at the Inria center in Paris. I was very satisfied with the results obtained during this internship and I was also very happy with François's guidance. That is how I decided to pursue a thesis under his supervision.
What was your path after your thesis? What position do you hold today?
After my thesis, I came to London to work as a postdoctoral researcher in the group led by Azalea Raad at Imperial College. I am working on a subject that is quite different from what I did in my thesis, allowing me to broaden my understanding of the field. More specifically, I'm doing research on weak memory models. When several tasks are executed at the same time, which is possible thanks to so-called multi-core processors, it is tempting to want to explain their possible results as if they had come from a single program alternating between these different tasks. This is not possible, however, because real processors behave in much more complex ways to achieve efficiency. The goal of weak memory models is precisely to give a more adequate description of what real processors can do.