Victor LANVIN est lauréat 2022 d’un prix de thèse Génie de la Programmation et du Logiciel pour sa thèse intitulée A Semantic Foundation for Gradual Set-Theoretic Types. Rencontre avec cet ancien doctorant de l’IRIF.

© GDR GPL. Victor Lanvin (à droite) et les deux autres lauréats des prix de thèse Génie de la Programmation et du Logiciel

Je m'appelle Victor Lanvin, après avoir intégré l'ENS Paris-Saclay en 2013, j'ai rapidement découvert ma passion pour les langages de programmation, et j'ai donc réalisé un stage de M2 avec Giuseppe Castagna à l'IRIF. Mon stage s'est prolongé sur une thèse de septembre 2017 à novembre 2021, toujours sous la direction de Giuseppe Castagna à l’IRIF. Depuis, j'ai rejoint l’entreprise du métavers social - Meta en mai 2022 en tant qu'ingénieur spécialisé dans les langages de programmation, compilateurs, et systèmes de types.

Je suis arrivé à l'IRIF en mars 2016, dans le cadre d'un stage de recherche en Master 2, avec Giuseppe Castagna, qui deviendra ensuite mon directeur de thèse. Je m'y suis immédiatement plu : l'ambiance entre doctorant·es et chercheur·euses est particulièrement agréable. Quel que soit le problème que l'on rencontre, en lien avec la recherche, un problème personnel ou administratif, il y a toujours quelqu'un capable de nous aider. La diversité des domaines de recherche abordés à l'IRIF est particulièrement stimulante. Les séminaires organisés chaque semaine sont une superbe occasion de découvrir de nouvelles thématiques de recherche, voire d'initier des collaborations parfois inattendues. Mon directeur de thèse, Giuseppe Castagna, m'a remarquablement bien accompagné durant ces cinq années. Il a su me guider dans le monde de la recherche et m'a soutenu dans les moments les plus difficiles de la thèse.

Dans ma thèse, je m'intéresse à ce qu'on appelle des systèmes de types pour des langages de programmation. Quiconque ayant utilisé un ordinateur (ou tout autre appareil électronique) sait qu'il y a parfois des bugs. Ces bugs sont souvent dus à des erreurs lors de l'écriture du code, et certains bugs peuvent coûter très cher (l'exemple classique est celui d'Ariane 5, ayant causé l'auto-destruction de la fusée et coûté plus de 350 millions de dollars). Ainsi, des outils sont développés pour détecter les bugs avant que ceux-ci ne prennent une ampleur démesurée. Les systèmes de types en font partie.

Dans un langage de programmation avec système de types, on associe à chaque valeur ou chaque donnée un “type”. Par exemple, on trouvera les types “entier”, “nombre à virgule”, ou “chaîne de caractères” (qui correspond aux mots ou phrases). Le système de types s'assure ensuite de la cohérence du programme. Par exemple, si on demande des informations sur un utilisateur, on va vérifier que son âge est bien un entier, et son nom une chaîne de caractères. On s'assure ainsi de détecter une grande classe de bugs avant même l'exécution d'un programme. Chaque système de types a ses avantages et inconvénients pour le programmeur, c'est donc pour cela qu'il existe beaucoup de recherches sur le sujet, et c'est dans ce cadre que s'inscrit ma thèse.

Lien vers sa thèse : A Semantic Foundation for Gradual Set-Theoretic Types

Les types ensemblistes sont des types pouvant faire intervenir des opérations d'union, d'intersection et de négation. Par exemple, si nous disposons d'un type “entier” et d'un type “nombre positif”, nous pouvons aussi construire le type “entier ET nombre positif” comme l'intersection des deux. Cela nous permet d'exprimer des propriétés plus précises sur les données que manipule un programme. Ici, nous pourrons donner à la valeur -4 le type “entier”, mais pas “nombre positif”. De même, nous pourrons donner à la valeur 3.14 le type “nombre positif”, mais pas “entier”. En revanche, nous pourrons donner à la valeur 5 le type “entier ET nombre positif”, ce qui donne beaucoup plus d'informations que simplement “entier” ou “nombre positif”. En allant plus loin, nous pouvons même donner à -4 le type “entier ET PAS nombre positif”, en utilisant les opérations d'intersection et de négation. Nous obtenons ainsi un système de types très expressif, qui nous donne des garanties fortes sur notre programme, au prix d'une complexité bien plus élevée pour le programmeur.

En contrepartie, le typage graduel est une approche moins sûre, mais bien moins complexe pour le programmeur. En résumé, le typage graduel permet à un programmeur d'omettre certains types dans son programme, et de laisser l'ordinateur vérifier la cohérence du programme automatiquement. Cela permet au programmeur de gagner du temps, parfois précieux, mais a l'inconvénient de laisser passer des bugs qui ne seront détectés possiblement qu'après l'exécution du programme. Outre le gain de temps, l'avantage de cette approche est qu'elle permet une transition progressive (graduelle) entre un programme où tous les types ont été omis, et un programme complètement typé. C'est une approche extrêmement utile lorsque l'on a affaire à une grande base de code (parfois plusieurs millions de lignes) et que l'on souhaite y ajouter progressivement des types afin de la rendre plus sûre.

L'idée derrière l'approche de sous-typage sémantique est de considérer un type comme un ensemble de valeurs. Par exemple, le type “entier” représente l'ensemble de tous les nombres entiers. Le type “nombre positif” représente l'ensemble de tous les nombres positifs (à virgule ou non). Cela permet d'exprimer très simplement et efficacement des propriétés puissantes, en utilisant des opérations sur les ensembles, comme l'intersection ou l'union d'ensembles. Par exemple, l'intersection entre l'ensemble des nombres entiers et l'ensemble des nombres positifs nous donne l'ensemble des nombres entiers positifs, et correspond exactement à l'intersection des types “entier” et “nombre positif” dans un programme. La théorie des ensembles ayant quelques siècles d'avance sur la théorie des langages de programmation, cela nous permet de réutiliser de nombreux résultats et théorèmes existants dans notre théorie. Dans ma thèse, nous avons adapté cette approche à la fois aux types ensemblistes et aux types graduels, afin d'en proposer une théorie unifiée.

Il existe encore de nombreuses bases de code qui ne contiennent aucun type et dans lesquelles se cachent de nombreux bugs. Ces bases de code ont souvent plusieurs décennies et peu de gens sont capables de les comprendre dans leur totalité, les programmeurs originels n'étant souvent plus disponibles. Ainsi, y dépister des bugs peut s'avérer extrêmement long et coûteux, et réécrire ce code est une tâche souvent risquée. Y ajouter un système de types est un bon moyen d'y dénicher et corriger des bugs sans pour autant avoir besoin de comprendre l'entièreté du code. Le principal avantage du typage graduel est qu’il est possible de travailler très progressivement sur le code, ce qui fait du typage de plusieurs millions de lignes de code une tâche abordable. L'avantage du sous-typage sémantique et des types ensemblistes est qu'ils permettent de s'adapter à des bases de codes très complexes, qui n'ont initialement pas été développées pour être typées plus tard.

Je suis désormais ingénieur chez Meta (anciennement Facebook) où et je travaille sur le développement d'un système de types pour Erlang, un langage initialement non-typé. Au quotidien, j'applique plus ou moins directement les travaux de ma thèse. Voir ces travaux mis en œuvre sur des bases de code aussi larges que celles disponibles chez Meta est pour moi très stimulant.