Développement web : concilier sûreté et flexibilité avec le typage graduel
Être typé ou non typé, telle ne sera plus la question ! Jusqu’à maintenant, les langages pouvaient être classifiés comme « typés », s’ils appliquaient certaines règles de contrôle a priori de leur exécution, ou « non typés ». Le typage graduel (gradual typing), qui permet d’avoir un contrôle des types uniquement sur certaines parties du programme, suscite beaucoup l’intérêt de grands acteurs de la technologie de l’information comme Facebook et Microsoft qui développent des versions graduellement typées des langages de programmation qu’ils utilisent. Grâce aux travaux de Victor Lanvin, les développeurs pourront désormais contrôler de manière plus fine et plus précise l’utilisation du typage graduel dans leurs programmes, permettant d’introduire plus de sûreté et de flexibilité ! Il a été récompensé pour son article « Gradual Set-Theoretic Types », distingué à la 1ère place dans la catégorie Undergraduate de l’ACM Student Research Competition. Son prix lui sera remis dans le cadre de la cérémonie du Turing Award.
Les langages de programmation se différencient entre langages typés ou non. Le typage « statique » d’un langage assure un certain contrôle a priori de son exécution. « Si on faisait un parallèle avec la physique, c’est comme si l’on s’assurait que l’on ne mélangeait pas des unités de mesure », précise Victor Lanvin, étudiant à l’ENS Paris-Saclay. L’addition par exemple doit se faire dans la même unité de mesure (des mètres avec des mètres), tandis que la division crée une nouvelle unité de mesure (des mètres et des secondes donnent une mesure en mètre par seconde). « Le fait que le programme soit typé assure ainsi en quelque sorte la cohérence des « unités de mesure » prises en charge par le langage, prouvant certaines propriétés, notamment que le langage ne produira jamais une certaine classe d’erreurs », développe-t-il. En effet, une incohérence n’est pas forcément visible dans un programme. Pour les langages non typés de telles erreurs peuvent ainsi ne se révéler qu’à l’exécution du programme… ce qui peut être très problématique !
L’utilisation de langages typés pourrait donc paraître préférable… mais sa mise en application peut apparaître particulièrement complexe en particulier dans le contexte du développement web où la souplesse des langages non typés est préférée. Le typage graduel, qui permet à un programmeur de choisir à quel point il souhaite que son programme soit typé, en fonction des parties de son programme qui nécessitent plus de sûreté, a été développé dans ce but. Les travaux de Victor Lanvin dans son article « Gradual Set-Theoretic Types » rendent l’utilisation du typage graduel plus puissante en permettant une application plus précise et contrôlée du typage graduel.
Pour cela, Victor Lanvin a fait le parallèle entre la théorie des ensembles mathématiques, comme l’ensemble des entiers par exemple, et les types dans les langages de programmation. « En appliquant cette théorie, il est possible d’utiliser ses opérations et ses résultats qui sont bien connus, directement dans la vérification des langages de programmation », indique Victor Lanvin. Ainsi, tous les programmes qui renvoient un entier pourront être classifiés dans l’ensemble des entiers par exemple. Cette approche permet de considérer des unions et des intersections d’ensembles, ce qui permet de développer le programme plus finement en fonction des besoins. Ainsi, un programme qui comprend une condition (« if » condition alors donne A, sinon donne B) pourra être classifié dans l’union des types de A et de B, car le programme peut produire les deux résultats. De la même manière, si l’on reprend l’exemple des mesures, un programme qui peut donner des résultats en mètre/seconde et en kilomètre/heure sera dans l’intersection de ces deux types.
« Ce que Victor Lanvin a résolu était mathématiquement très difficile, s’enthousiasme Giuseppe Castagna, qui a encadré ses travaux au sein de l’Institut de Recherche en Informatique Fondamentale (IRIF - CNRS/Université Paris-Diderot). Le typage graduel était jusqu’à maintenant étudié principalement de manière syntaxique, c’est-à-dire que l’on étudiait les symboles mais pas leur signification mathématique. Son tour de force est de donner une interprétation mathématique des symboles, notamment en théorie des ensembles, pour en déduire des propriétés. Cela apporte non seulement une fondation mathématique au typage graduel mais possède aussi une valeur pratique importante pour la mise en place de cette méthodologie, par exemple pour le développement web. »
À partir de septembre 2017, Victor Lanvin poursuivra ses recherches dans une thèse encadrée par Giuseppe Castagna au sein de l’IRIF. Les travaux qui ont donné lieu à son prix seront présentés dans un article qui a été accepté à ICFP, la conférence de référence en langages de programmation fonctionnels, qui se tiendra début septembre 2017.
Prix de l’ACM Student Research Competition
Pour reconnaître la valeur de la participation des étudiants aux conférences, ACM a lancé le Student Research Competition Program en 2003. Pour cette édition 2017, les lauréats se sont distingués parmi plus de 330 étudiants qui ont présenté leurs recherches dans 24 conférences ACM. Victor Lanvin a obtenu le premier prix de la catégorie undergraduate. Parmi les 6 lauréats (3 doctorants et 3 undergraduates), Victor Lanvin est le seul qui ne soit pas dans une université des États-Unis. Sa distinction lui sera remise lors de la cérémonie du Turing Award le 24 juin 2017.