Escaping the Quicksand: A Call to Arms

Imaginez un monde où la machinerie invisible de la vie moderne — nos banques, nos hôpitaux, nos réseaux électriques et nos réseaux de communication — est construite sur une fondation qui s'enfonce lentement. C'est la réalité à laquelle l'industrie informatique est confrontée aujourd'hui. Pendant des décennies, la méthode standard pour construire un logiciel a consisté à écrire une description approximative de ce qu'un programme doit faire, puis à écrire le code, et enfin à le tester en l'exécutant avec diverses entrées pour voir s'il casse. Cette méthode, connue sous le nom de développement par test et débogage, a permis à la technologie de prospérer, mais elle laisse les systèmes truffés de failles cachées. Parce que les descriptions originales sont souvent vagues et rédigées en langage ordinaire, elles ne peuvent pas être vérifiées par des machines, et parce que les tests ne peuvent couvrir qu'une infime fraction des milliards de façons possibles dont un programme pourrait se comporter, de nombreuses erreurs passent entre les mailles du filet. À mesure que l'intelligence artificielle commence à écrire davantage de code, ce cycle menace de s'accélérer, créant de nouveaux systèmes encore plus vastes, complexes et fragiles qu'auparavant, bâtis sur des « sables mouvants » de choix de conception vieux de plusieurs décennies, faits à une époque où les cyberattaques étaient rares et la puissance de calcul limitée.

Deux chercheurs, Peter Sewell de l'Université de Cambridge et Jean Pichon-Pharabod de l'Université d'Aarhus, soutiennent que l'industrie est coincée dans une boucle dangereuse depuis soixante-quinze ans. Ils observent que si nous sommes devenus incroyablement habiles à écrire du code, nous avons négligé les définitions précises de ce que ce code est censé accomplir. L'approche actuelle repose sur des spécifications en prose : des paragraphes de texte qui décrivent le comportement d'un système. Bien que ces textes soient faciles à lire pour les humains, ils sont intrinsèquement ambigus et incomplets. Un lecteur humain peut interpréter une phrase d'une certaine manière, tandis qu'une machine ou un autre humain l'interprétera différemment. Parce que ces descriptions ne peuvent pas être directement testées par un ordinateur, les développeurs sont contraints de deviner quel est le comportement correct, s'appuyant souvent sur des vérifications simples comme « est-ce que le programme plante ? » plutôt que de vérifier si le programme fait réellement ce qu'il doit faire. Ce fossé entre l'intention écrite et le code réel crée une énorme dette technique, un coût caché qui se manifeste par des vulnérabilités de sécurité et des défaillances de systèmes exploitables par des attaquants.

Les auteurs suggèrent que la solution n'est pas d'abandonner les tests, mais de changer la façon dont nous utilisons les spécifications. Au lieu d'écrire des paragraphes vagues, ils proposent de créer des spécifications exécutables, c'est-à-dire écrites d'une forme que l'ordinateur peut exécuter. Imaginez une spécification qui agirait comme un arbitre en direct pendant le processus de développement. À mesure que le code est écrit ou généré, cette spécification exécutable fonctionne parallèlement à lui, vérifiant instantanément si le comportement du code correspond aux règles prévues. Si le code tente de faire quelque chose que la spécification interdit, le système le signale immédiatement. Cela crée une boucle de rétroaction beaucoup plus serrée, permettant aux développeurs de détecter les erreurs au moment où elles se produisent, plutôt que des semaines plus tard. Cette approche peut être appliquée de différentes manières : on peut commencer par le code et écrire une spécification pour l'assortir, commencer par une spécification et générer un code qui s'y conforme, ou construire les deux ensemble. La clé est que la spécification n'est pas seulement un document à lire, mais un outil à utiliser.

Cependant, les chercheurs reconnaissent qu'il ne s'agit pas d'un simple interrupteur à actionner. Pour que cela fonctionne à grande échelle, la communauté informatique doit construire une nouvelle couche d'infrastructure. Actuellement, il n'existe pas de définitions universellement acceptées et lisibles par machine pour le comportement de nombreuses technologies fondamentales, telles que le langage de programmation C, le langage Rust ou les instructions qui font tourner les puces informatiques. Bien que certains chercheurs aient réussi à créer ces définitions pour des parties spécifiques du système, il n'existe pas de cadre unifié pour les relier tous. Les auteurs soulignent que la construction de cette infrastructure est un défi d'échelle et de coopération. Cela nécessite un effort massif et coordonné de la part des universités, des gouvernements et des entreprises technologiques pour créer, valider et maintenir ces définitions précises pour toute la pile technologique, du matériel jusqu'aux services cloud.

L'article aborde également le rôle de l'intelligence artificielle. Les auteurs avertissent que le simple fait d'utiliser l'IA pour écrire plus de code sans ces meilleures boucles de rétroaction ne fera qu'aggraver le problème. L'IA peut générer du code plus rapidement que les humains, mais si ce code est construit sur des fondations fragiles et testé uniquement avec les anciennes méthodes inefficaces, elle ne fera que créer des systèmes plus vastes avec davantage d'erreurs cachées. Inversement, si l'IA est utilisée pour aider à générer et à vérifier ces spécifications exécutables, elle pourrait devenir un outil puissant pour améliorer la qualité des logiciels. Les auteurs envisagent un avenir où l'IA aide à créer des spécifications rigoureuses, et où ces spécifications sont utilisées pour vérifier que le code, qu'il soit écrit par l'homme ou par l'IA, est correct. Cela permettrait une augmentation graduelle de la confiance, passant de tests simples vers des preuves mathématiques de correction plus complexes, le tout sans exiger que chaque développateur devienne un mathématicien.

Malgré la voie claire qui se dessine, les auteurs soutiennent que l'industrie est freinée par un décalage d'incitations. Les entreprises technologiques sont motivées par la sortie rapide de produits pour capturer des parts de marché, tandis que les risques d'échec retombent largement sur la société et les utilisateurs finaux. Construire l'infrastructure robuste nécessaire pour prévenir ces échecs est coûteux et chronophage, et aucune entreprise ne veut assumer seule le coût total de la résolution de problèmes qui affectent tout le monde. Les chercheurs appellent à un effort collectif, similaire aux grands projets de la physique ou de la biologie, pour financer et coordonner la création de cette infrastructure sémantique. Ils suggèrent que, bien que le coût soit important, il ne représente qu'une infime fraction des dépenses actuelles consacrées à l'intelligence artificielle et qu'il est essentiel pour sécuriser l'avenir de l'informatique. Sans ce changement, l'industrie reste piégée dans un cycle de construction de systèmes de plus en plus complexes sur des fondations trop faibles pour les soutenir, laissant la société vulnérable à un risque constant.

Les auteurs concluent que les outils et les méthodes pour résoudre ce problème existent déjà. Des chercheurs ont démontré avec succès comment définir le comportement de systèmes complexes et les vérifier avec un haut degré de confiance. Ce qui manque, c'est la volonté de mettre ces méthodes en pratique courante et de construire l'infrastructure partagée qui les rend accessibles à tous. Le papier sert d'appel à l'action pour la communauté de la recherche, les chefs de file de l'industrie et les organismes de financement afin qu'ils collaborent à cette tâche. En passant de descriptions vagues à des spécifications précises et exécutables, le monde de l'informatique peut échapper aux sables mouvants de la dette technique et construire un avenir qui soit non seulement plus innovant, mais aussi fondamentalement plus sûr et plus fiable.