211service.com
Code garanti
Ariel Davis
Adam Chlipala, professeur agrégé d'informatique au MIT, pense qu'il existe une meilleure façon d'écrire des programmes informatiques.
La plupart des programmes répertorient simplement les opérations que l'ordinateur doit effectuer lorsqu'il reçoit des types de données particuliers. Le programmeur doit écrire des tests pour déterminer si un programme fait ce qu'il est censé faire, et comme il est pratiquement impossible de prédire toutes les façons dont un programme pourrait être utilisé, la plupart des logiciels ont des bogues.
Chlipala préfère la programmation dite fonctionnelle. Au lieu d'enchaîner des commandes impératives, un programmeur fonctionnel définit un ensemble de fonctions ou de relations mathématiques entre les entrées et les sorties. Essentiellement, la programmation fonctionnelle exprime ce que fait un programme sous la forme d'un ensemble d'équations.
Considérer les programmes comme des combinaisons de fonctions peut ne pas être intuitif, mais pour les personnes pour lesquelles ils travaillent, c'est vraiment un formidable outil d'amélioration de la productivité, dit Chlipala. D'une part, cela peut éliminer les tests. Les programmes fonctionnels sont si mathématiquement précis qu'il est relativement simple de les vérifier, ou de prouver qu'ils font ce qu'ils devraient, automatiquement.
L'un des Chlipala principaux intérêts de recherche élargit le champ de la vérification automatique. Par exemple, les outils de vérification que lui et ses collègues ont développés ont permis de créer le premier système de fichiers - la partie d'un système d'exploitation qui régit le stockage des données - garantissant de ne pas perdre les données du programme lors d'un plantage du système.
Un autre avantage des langages fonctionnels est qu'ils éliminent une grande partie du travail fastidieux de la programmation. Encore une fois, parce que les programmes fonctionnels sont si précis, il est facile pour les compilateurs - les programmes qui transforment le code en fichiers exécutables - de déterminer comment les faire fonctionner le plus efficacement.
L'un des outils les plus populaires de Chlipala est un langage fonctionnel appelé Ur/Web, le seul langage de programmation qui permet aux programmeurs de spécifier toutes les fonctionnalités d'une application Web dans un seul programme. Le compilateur d'Ur/Web génère ensuite automatiquement le code XML, le code JavaScript et les requêtes de base de données nécessaires pour implémenter l'application. Il s'assure également que ces différents composants interagissent correctement.
Ur/Web est similaire à d'autres langages fonctionnels, mais il ajoute des fonctionnalités de sécurité qui lui permettent de boucher automatiquement les failles courantes dans les applications Web. Par exemple, il peut garantir qu'une partie de son code importé dans une section d'une page (comme une publicité) ne peut pas en espionner une autre (comme un outil de calendrier).
Comme de nombreux informaticiens dans la trentaine, Chlipala s'était essayé à l'écriture de jeux vidéo au lycée. Mais cette entreprise l'a rapidement conduit dans une autre direction. Quand il était étudiant de première année, ses tentatives d'écrire des jeux pour la calculatrice graphique de Texas Instruments l'ont amené à développer un compilateur pour l'appareil.
Il a continué à se concentrer sur les compilateurs en tant qu'étudiant de premier cycle à l'Université Carnegie Mellon, et lors de son premier semestre en tant qu'étudiant diplômé à l'Université de Californie à Berkeley, son futur directeur de thèse lui a demandé s'il aimerait contribuer à un projet sur ordinateur- vérification assistée. Chlipala est immédiatement devenu accro.
Il y a un certain type de personnalité paranoïaque qui devient accro à ce genre de travail, et c'est définitivement moi, dit-il. Il n'y a pas beaucoup de choses qui sont absolument sûres dans ce monde, mais quand vous faites des preuves vérifiées par machine sur les programmes, vous vous en approchez assez.