Delia Kesner : « Spécifier l’aspect quantitatif des données pour construire des langages de programmation plus efficaces »

On entend beaucoup parler de la fiabilité des logiciels. Qu’est-ce que votre approche apporte de plus ?

Delia Kesner : C’est vrai que les logiciels sont maintenant omniprésents dans nos vies, dans les domaines du transport, de la médecine, des télécommunications, du système bancaire, des réseaux sociaux… A tous ces logiciels, on leur demande beaucoup plus que de seulement fonctionner. Il faut qu’ils soient fiables, c’est-à-dire qu’il n’y ait pas d’erreurs dans leur exécution, notamment pour les erreurs des logiciels qui peuvent avoir des conséquences désastreuses sur les vies humaines (avion, appareils médicaux, …) ou même au niveau financier. Mais on leur demande aussi de consommer moins (en espace mémoire, en électricité) et d’être plus rapide. C’est sur cette 2^e partie que j’interviens.

Pour le 1^er point, sur la fiabilité, le problème c’est que les développeurs et les ordinateurs ne parlent pas la même langue, et que même si les développeurs utilisent les langages de programmation pour « s’exprimer », il y a tout de même des biais ! Quand j’écris une instruction dans un programme censé avoir un effet concret selon la description du langage de programmation dans lequel ce programme est écrit, il faudrait que celui-ci s’exécute sur l’ordinateur comme je l’avais en tête. Ça paraît évident, mais ce n’est pas vraiment le cas dans la réalité ! De là est née la sémantique des langages de programmation. Il s’agit de construire et de spécifier des langages qui éliminent toutes les « incompréhensions » entre développeurs et programmes.

Mais il est impossible d’étudier les propriétés des programmes d’un point de vue purement syntaxique, ce qui reviendrait à s’attacher aux symboles sans se préoccuper du sens. Avec une approche sémantique, on se concentre sur la compréhension de l’intention du développeur, et le but est que la sémantique que le développeur a en tête soit vraiment celle interprétée par l’ordinateur.

Dans les langages de programmation, il y a les instructions dont nous venons de parler, mais aussi les données car les instructions manipulent des données. Les données sont classifiées selon différents « types », car on ne les manipule pas de la même façon s’il s’agit d’un nombre entier ou d’une chaîne de caractères. Par exemple, pas d’opération arithmétique sur une chaîne de caractères, sinon le logiciel devient incohérent ! Certains bugs célèbres dans l’histoire du logiciel viennent justement d’un programme qui a utilisé un mauvais type de données à un endroit où il s’attendait à un autre type de données.
Jusque-là, la théorie des types, qui classifient les données, s’était beaucoup concentrée sur l’aspect qualitatif des données (entier ou chaîne de caractères…). Je travaille dans une thématique qui a émergée depuis une quinzaine d’années et qui s’intéresse aussi à son aspect quantitatif.

Qu’est-ce que peut apporter un point de vue quantitatif à la sémantique des langages de programmation ?

D. K. : Passer dans le monde quantitatif apporte plus d’informations intéressantes dans un langage de programmation. Comme nous l’avons dit, en informatique moderne, on ne veut pas seulement écrire des programmes qui fonctionnent, on souhaite aussi qu’ils soient efficaces, c’est-à-dire exécutables en un minimum de temps, et qu’ils occupent moins d’espace mémoire. L’efficacité se retrouve dans ces informations de quantitativité. Pour savoir si un programme est efficace ou non, il nous faut des données quantitatives pour pouvoir mesurer le temps et l’espace consommé.

Le but de mon projet est de définir des systèmes de type quantitatifs pour les langages de programmation modernes dits de « haut niveau », en opposition aux langages de bas niveau come l’assembleur par exemple, qui sont proches du langage machine. Dans un langage haut niveau, il y a un niveau d’abstraction très élevé qui permet au développeur d’être extrêmement concis, car une instruction cache toute une complexité d’actions de bas niveau. Comme il est très difficile de traiter de manière quantitative toute la richesse expressive d’un langage haut niveau, j’attaque d’abord le problème de la quantitativité en isolant une seule caractéristique ou primitive à la fois. J’étudie chaque « brique de base » qui peut être par exemple une primitive de filtrage, un opérateur de contrôle ou encore la manipulation de données infinies, et j’analyse ce qui se passe d’un point de vue quantitatif pour chacune de ces briques. Mon but est de définir un système de types d’un point de vue quantitatif pour vérifier certaines propriétés du langage de programmation sous-jacent. Par exemple une propriété typique est celle de la terminaison, les systèmes de types ne vont pas seulement garantir qu’un programme va terminer, mais en ajoutant des données quantitatives, ils garantiront qu’il va terminer en exactement n pas d’exécution.