La recherche en langages de programmation au quotidien

Dans le cadre de mon travail j’ai été amené à écrire un petit texte qui explique mon quotidien fait de "recherche (scientifique) en langages de programmation". Je me permets de le diffuser ici au cas où ça intéresse des gens.

Ma recherche

Je travaille à l’INRIA, un institut public français de recherche en informatique. Je fais de la programmation et de la recherche sur les langages de programmation.

Mon rôle est d’étudier ces langages, de mieux les comprendre, pour identifier les propriétés désirables et capturer des éléments de langage qui sont les plus simples, performants et sûrs à utiliser. Cela permet faire évoluer les langages déjà existants, voire même de créer un langage où il est plus facile de dire à la machine ce que l’on veut qu’elle fasse, et où la machine est aussi mieux capable de vérifier que notre demande est cohérente.

(Pour plus d’information sur l’étude mathématique des langages de programmation, voir le précédent billet Pourquoi la recherche en langages de programmation ?.)

Ma recherche est aussi liée au développement des assistants de preuve, des outils qui permettent non pas d’écrire des programmes et de les faire faire exécuter par l’ordinateur, mais d’écrire des preuves mathématiques et de les faire vérifier par l’ordinateur. L’interaction entre langages de programmation et assistants de preuves est double. D’une part, beaucoup de travaux sur les langages de programmation peuvent être réutilisés pour comprendre les « langages de preuve » des assistants de preuve. D’autre part, nous essayons de concevoir des langages dans lesquels on puisse donner une spécification du comportement de son programme, et aider ensuite l’ordinateur à vérifier, à prouver que la spécification est vérifiée par le programme – ces langages intègrent donc des outils de recherche de preuve et d’assistance à la preuve.

L’équipe de recherche dans laquelle je travaille, nommée Parsifal, étudie la théorie de la démonstration, c’est-à-dire l’étude formelle des preuves mathématiques. Certains mathématiciens étudient les nombres, les événements aléatoires ou les surfaces géométriques, nous étudions les preuves mathématiques elles-mêmes comme des objets formels. C’est un sujet essentiel pour comprendre la recherche de preuve, les assistants de preuve, mais qui a aussi des applications nombreuses pour étudier les langages de programmation : en regardant d’une certaine façon peut voir qu’un « programme » est aussi une « preuve » et inversement. J’utilise cette correspondance preuves-programmes dans mon travail et j’espère continuer à la développer.

Mon quotidien

Au jour le jour, ma façon de travailler ressemble à celle des mathématiciens et mathématiciennes : j’essaie de comprendre quels résultats je veux établir, et ensuite comment les prouver. Un article scientifique dans mon domaine commence typiquement par expliquer un problème perçu dans un langage de programmation donné, une proposition de solution, puis donner une définition mathématique du langage corrigé, et montrer un théorème qui nous convainc que le problème n’est plus présent. Souvent, on ne travaille pas sur un langage existant en entier, mais sur une version simplifiée, conçue pour garder uniquement les aspects que nous souhaitons étudier.

Bref, je peux présenter mon travail de recherche avec des définitions, des lemmes et des théorèmes. Mais souvent je vais aussi essayer d’implémenter les langages et les programmes considérés, pour pouvoir exécuter des exemples sur un ordinateur, comprendre certaines propriétés de l’exécution, et aussi garder un lien de praticien avec l’activité de programmation que j’étudie.

Concrètement, vous pouvez voir sur les images ci-dessous à quoi ressemble une session de travail sur Abella, un nouvel assistant de preuve en cours de développement au sein de l’équipe Parsifal. On voit à gauche une zone bleue qui représente la partie déjà vérifiée par l’outil (les preuves dans cette partie sont correctes), une zone noire qui n’a pas encore été vérifiée (on est en train d’écrire la preuve), et à droite on voit le "but" courant, ce qu’il reste à faire vérifier pour conclure la preuve :

une interface d’assistant de preuve

Les assistants de preuve ont vocation à être utilisés par tous les scientifiques faisant des raisonnement mathématiques, mais il reste du travail pour qu’ils soient plus faciles à utiliser – ils sont aujourd’hui réservés aux spécialistes du domaine. Ma communauté de recherche fait des efforts pour adopter ces outils, je m’en sers parfois pour valider mon propre travail, et cela permet de découvrir des problèmes d’utilisation, des points à améliorer pour pouvoir espérer une adoption plus grande. Aujourd’hui quand quelqu’un annonce un nouveau résultat mathématique, il peut être très difficile de savoir si le résultat est correct ou non ; il sera peut-être un jour réaliste de demander à la personne de fournir une preuve vérifiée par un assistant de preuve, pour accélérer son étude et sa compréhension par les scientifiques du domaine.

Échanger avec l’extérieur

De nouveaux langages de programmation apparaissent tous les ans. Une partie est construite par des scientifiques du domaine, ou des gens qui ont étudié notre travail, mais la majorité vient de personnes spécialistes d’un tout autre domaine de la programmation, qui veulent créer un bon langage pour leurs besoins, sans avoir étudié la théorie.

Une partie de notre travail consiste donc à entrer en contact avec les personnes qui créent de nouveaux langages et les utilisent, pour leur transmettre de bonnes pratiques de conception, les alerter sur des problèmes à venir, et aussi découvrir de leurs besoins et idées pour faire évoluer notre compréhension commune des langages de programmation. Nous avons parfois des discussions directes avec l’équipe qui conçoit un langage, et il nous arrive même de travailler scientifiquement sur ces nouveaux langages (récemment ma communauté s’est penchée sur les langages R, Ceylon, Rust et Julia par exemple), mais nous avons aussi un impact indirect, en faisant utiliser des langages conçus par notre communauté dont certaines idées inspirent ensuite les nouveaux langages de programmation. Étudier les nouveaux langages de non-spécialistes nous permet aussi de découvrir de nouveaux besoins qui viennent enrichir notre activité de recherche.

Ainsi, je travaille sur le langage de programmation OCaml (comme scientifique et aussi comme contributeur et co-mainteneur de l’implémentation), conçu à l’INRIA et encore développé en grande partie dans l’institut. Le langage est utilisé dans des projets venant de tous les horizons, la recherche, le logiciel libre et l’industrie, qui font connaître ses idées à un public plus large. L’idée de programmation « fonctionnelle », mettant l’accent sur l’importance de raisonner rigoureusement sur son code, est promue par OCaml mais aussi d’autres langages comme Scala, Haskell, ou le langage F# (dérivé de OCaml), et influence les évolutions de langages grand public comme Java, C# ou Javascript.

un exemple de code OCaml

Recherche et logiciel libre

Les résultats de mes travaux sont accessibles à tous – pour moi c’est une part essentielle du contrat moral de la recherche publique. Mes publications sont en accès libre (et archivées sur arXiv et/ou HAL (si possible en licence CC-BY, mais malheureusement ce n’est pas toujours moi qui décide), et le logiciel produit est sous licence libre.

Dans le cadre de mon activité de recherche, je produis surtout des petits prototypes qui ne sont pas forcément très intéressants pour les autres – même s’il m’arrive de partager effectivement du code avec d’autres chercheurs ou de collaborer sur leurs projets. Mon activité de développement principale tourne autour de l’implémentation du langage OCaml, et d’outils et bibliothèques de son écosystème (je travaille là-dessus dans une zone assez floue entre le temps libre/personnel et le temps de travail).

Le compilateur OCaml est un logiciel libre, et j’essaie (ainsi que les autres mainteneurs) de faire des efforts pour encourager les contributions externes – faire des revues de code pour les contributeurs externes, marquer des bugs comme "faciles" sur le bugtracker, organiser des réunions d’initiation à la contribution.

Un langage de programmation qui a des utilisateurs n’est pas un projet libre facile à gérer : il faut être très prudent quand on accepte de nouvelles fonctionnalités pour préserver la compatibilité arrière et éviter l’enfouissement sous les fonctionnalités (feature bloat). Du coup il peut être très difficile de juger des propositions de changement et de prendre des décisions, ce qui frustre les contributeurs. Une nouvelle fonctionnalité peut attendre dans un coin pendant des années parce qu’elle n’est "pas complète", voire même parce qu’il y a deux propositions de syntaxe différentes et qu’on ne sait pas laquelle on préfère. Ce n’est pas unique à OCaml; tout langage est beaucoup plus difficile à évoluer qu’il n’y paraît au premier abord. C’est une raison de plus de bien faire attention à la théorie quand on conçoit un langage ou une nouvelle fonctionnalité, pour essayer d’avoir la meilleure première version possible :-)

Ces derniers temps j’ai aussi eu l’occasion de faire un peu de gestion des publications de nouvelle version (release management), à l’occasion en particulier d’un congé parental pris par le gestionnaire de nouvelles versions habituel, Damien Doligez. Le plus difficile dans cette partie du travail est de décider comment réagir en cas de problème repéré tard dans le cycle de développement, et d’évaluer la sûreté et les risques pour la compatibilité arrière des correctifs proposés – un correctif risque toujours d’introduire de nouveaux problèmes.



11 commentaires

Super intéressant ! C’est pas la première fois que j’entends parler de l’INRIA et ça m’a l’air bien cool comme institution. :)

Les résultats de mes travaux sont accessibles à tous – pour moi c’est une part essentielle du contrat moral de la recherche publique. Mes publications sont en accès libre (et archivées sur arXiv et/ou HAL (si possible en licence CC-BY, mais malheureusement ce n’est pas toujours moi qui décide), et le logiciel produit est sous licence libre.

<3

+0 -0

Merci beaucoup ! Super intéressant. (y’a vraiment des super billets en ce moment !!!)

J’avais vu une présentation de Martin Odersky sur dotty (Scala 3, appelons-le comme ça), dans laquelle il indiquait qu’une des avancées majeures avaient été de pouvoir définir un sous-ensemble du langage (appelé DOT) qui pouvait être formellement prouvé (en Coq). Et qu’il en découlait que certaines fonctionnalités du langage (genre les projections de type, dont je n’ai jamais compris l’intérêt) devaient être supprimées pour que DOT puisse être sain, et formellement prouvé.

C’est un peu mystique pour moi tout ça, en tant qu’utilisateur je trouve chouette certaines features de dotty (union / intersection types nativement, etc.). Mais ça m’intéresserait vachement, si jamais tu en as envie, que tu nous donnes ton point de vue sur leur démarche, comment elle se rapproche de ce que tu fais, etc. (si ça te botte hein !! bien sûr).

Merci en tout cas :)

+0 -0

Les gens qui travaillent sur la théorie de Scala (à commencer par Martin Odersky, mais il y a plusieurs chercheurs et chercheuses sur ce sujet, par exemple Nada Amin et Tiark Rompf) font partie de la même communauté de recherche et ils travaillent avec les mêmes méthodes et outils; ce sont mes collègues.

Scala est peut-être un peu particulier en cela que c’est un langage qui se veut vraiment "industriel", avec une volonté d’adoption forte, beaucoup de gens qui travaillent sur l’implémentation, les bibliothèques et la communauté (il y a nettement plus de gens qui travaillent sur l’implémentation Scala à temps plein que sur OCaml par exemple – mais moins que sur Java), et des gens qui sont un peu à cheval entre les deux mondes. Le projet "DOT" est vraiment un projet de recherche, il me semble que "Dotty" est avant tout un projet de ré-ingénérie d’une implémentation devenue trop difficile à maintenir – mais qui a la chance de reposer aussi sur les avancées théoriques de DOT.

Enfin, une dernière chose à dire c’est que DOT est un projet peut-être plus ambitieux que d’autres approches de la formalisation des langages de programmation; d’habitude, on cherche à exprimer un langage en le traduisant vers un ensemble de composants déjà bien étudiés par la communauté (les lambda-calculs typés), et en montrant comment on peut reconstruire le langage à partir de ces briques et utiliser des approches classiques pour montrer que le design est raisonnable (que le système de type fait sens, par exemple). DOT a utilisé une approche différente qui est de concevoir un nouveau langage noyau (une nouvelle brique de base), plus adaptée à ce qu’était devenu Scala au fil du temps (qui a commencé comme une transformation incrémentale des langages ML pour ajouter de la programmation objet); en particulier, la preuve de correction du typage, qui a été faite seulement récemment (il y a un an ou deux) alors que DOT a déjà été proposé depuis plusieurs années, utilise une technique déjà connue mais relativement peu courante dans la communauté, moins standard.

Merci pour l’article !

Question naïve : c’est quoi la différence concrète entre Abella et Coq ? Je me suis penché un peu sur les articles mais la différence doit être trop directe pour les experts du domaine pour qu’on en fasse mention. Du coup vu que je ne suis qu’un utilisateur occasionnel de Coq (et que je ne connais pas la théorie sous-jacente), je ne vois pas ce qui les différencie.

(Comme @gasche l’a mentionné, il y a des travaux formels autour de Rust. Pour ceux que ça intéresse : http://plv.mpi-sws.org/rustbelt/ ).

Sur Abella et Coq, il y a des différences au niveau théorique (la fondation scientifique des deux outils est un peu différente) et au niveau pratique (principalement dues au fait que Coq est un projet plus gros et plus ancien, qui a reçu beaucoup de fonctionnalités importantes).

Au niveau théorique, on peut se demander pour chaque assistant de preuve sur quelle "logique" il se base pour vérifier les démonstrations : quelles sont les règles de raisonnement considérées comme valides.

Coq (et Agda, et Lean) utilisent une logique venant de la théorie des types dépendants, une certaine approche des mathématiques constructives, qui est très puissante mais aussi assez récente et pas forcément encore complètement comprises. Les principes fondamentaux n’ont pas changé depuis les années 70/80 où elles ont commencé à être utilisées pour des assistants de preuve, mais elles sont un sujet de recherche actif, elles continuent à évoluer en fonction des besoins et problèmes rencontrés par les assistants de preuve, et des avancées scientifiques imprévisibles (comme l’introduction de la théorie homotopique/univalente des types à la fin des années 2000). C’est excitant, mais en même temps il y a une part de risque : quand on fait évoluer ces théories il arrive qu’on fasse des erreurs, et qu’on passe par des étapes intermédiaires incohérentes – donc permettant en théorie d’accepter des preuves invalides.

Les assistants de la famille HOL (et Isabelle) utilisent la logique classique d’ordre supérieur et la théorie des ensembles, qui sont des fondements plus "standards" du point de vue des mathématiciens, qui évoluent beaucoup moins, mais sont considérés comme moins élégants par une partie des concepteurs d’assistants de preuve (ces logiques sont moins appropriées pour parler de constructions abstraites génériques).

Enfin, Abella descend d’une famille d’assistants de preuve un peu particulière, avec en particulier le système Twelf, construite sur l’idée de choisir des logiques adaptées à la description des langages de programmation, et en particulier au problème des variables : les programmes informatiques ont une structure de portée et liaison de variable qui les rend plus difficiles à manipuler que la plupart des objets mathématiques finis standards (arbres, graphes), et qui pose des difficultés dans la plupart des assistants de preuve classique. Abella utilise une logique qui introduit un quantificateur "nabla", à mi-chemin entre un quantificateur universel (pour tout x, la propriété P(x) est vraie) et un quantificateur universel (il existe un x tel que P(x) est vraie), qui introduit un nom frais (pour un nouveau nom x, P(x) est vraie). Le reste de la logique est au contraire très classique (logique intuitionniste et induction/coinduction), moins "originale" que les théories des types dépendants (ce qui est rassurant) mais aussi moins puissante pour la généricité.

Pour ce qui est de la pratique, Abella a beaucoup moins de bagage que Coq (ou Isabelle, etc.), et en particulier son langage de tactiques, qui décrit les preuves, est très pauvre comparé à celui de Coq. C’est sensiblement moins agréable à utiliser à l’usage (j’envisage parfois d’améliorer ça). Une autre différence importante est que Abella est construit par dessus un langage de programmation, lambda-prolog, qui est langage de programmation dit "logique" qui est très différent des langages de programmation classiques (même les langages fonctionnels, dont le langage de programmation interne de Coq, Gallina). Il est moins pratique pour certaines choses (pas excellent sur la généricité et la modularité), mais étonamment agréable pour certaines tâches de métaprogrammation qui arrivent naturellement dans notre domaine de recherche (quand on veut, par exemple, décrire et prouver les propriétés d’un système de typage pour un langage donné).

Au final, aujourd’hui je dirais que Abella n’est pas aussi généraliste qu’un système comme Coq, et que son langage de preuve le rend malcommode pour de gros développements, mais qu’il apporte un vrai confort sur un domaine spécifique qui correspond bien à mon domaine de recherche. Contrairement à ses prédecesseurs comme Twelf, il est cependant construit sur des bases assez générales, et on peut imaginer l’étendre pour devenir un assistant de preuve généraliste.

Après on peut se demander si ça vaut le coup d’investir du temps et des efforts dans un assistant de preuve supplémentaire. Je pense que c’est à chacun de faire ses choix, mais de toute façon il reste assez de choses à découvrir dans ce domaine pour qu’on soit amené à en re-développer régulièrement avec des idées nouvelles.

Ok, je vois mieux, merci. Ça explique aussi pourquoi en ce qui me concerne la différence n’est pas si incroyablement notable, j’utilise que les parties les plus simples de Coq. Et Coq commence à devenir une sacré usine à gaz.

Après on peut se demander si ça vaut le coup d’investir du temps et des efforts dans un assistant de preuve supplémentaire.

gasche

Sur ce point, pour moi la réponse reste oui. Rien que parce qu’un design de base très légèrement différent suffit souvent à créer de grosses différences à l’usage qui nous en apprennent encore, mais aussi simplement parce que ça permet de nous donner d’autre confirmations sur des connaissances "acquises".

C’est une question un peu plus compliquée que ça, pour au moins deux raisons.

D’une part, développer un assistant de preuve jusqu’à qu’il devienne utilisable en pratique demande des efforts d’ingénierie importants, qui sont portés par des chercheurs (et étudiant-e-s en thèse, etc.). C’est intéressant et important de se confronter à la pratique, mais cela tient aussi en partie du sacrifice : on prend sur son temps de recherche pour rendre service aux autres utilisateurs. Ce n’est pas réaliste d’espérer mener des efforts de ce type en parallèle sur un grand nombre de prouveurs. C’est un peu comme les langages de programmation : les équipes de recherche ont les compétences pour créer des langages variés et intéressants, mais pas les moyens humains de développer des IDEs, l’outillage, la documentation etc. pour tous ces langages. Il y a des gens qui essaient de réduire le coût de ces développements complémentaires pour les rendre accessibles à de plus petites équipes, mais ça fait longtemps qu’on cherche (pour les langages, pas pour les prouveurs) et on n’a pas de solution miracle. L’état des choses pourrait changer quand l’industrie (et/ou la communauté du logiciel libre ?) s’investira du problème, mais ça pourrait venir aussi avec une multiplication d’outils propriétaires, avec plus de marketing que d’arguments techniques, etc.

D’autre part, pour l’instant personne ne sait vraiment comment faire interopérer des preuves. Cela veut dire qu’à chaque nouveau prouveur qu’on développe, il faut refaire les développements formels dans ce cadre. Ça n’est pas un soucis pour des petits projets, mais aujourd’hui on commence à pouvoir et vouloir développer de vraies bibliothèques mathématiques contenant une partie importante des connaissances mathématiques, et le travail de redéveloppement pour chaque prouveur pourrait être colossal. On pourrait se retrouver dans un monde avec des résultats "perdus", des preuves formelles faites avec des assistants de preuve anciens qu’on n’arrive plus à connecter avec les mathématiques modernes, développées dans des assistants plus récents. Il y a des gens qui travaillent sur comment relier les assistants de preuve entre eux, mais c’est un problème très difficile – pour les langages de programmation, les Foreign Function Interfaces marchent bien pour binder des procédures à des types/interfaces très simple, "prend un tableau de flottants et renvoie un entier", et nettement moins bien pour des types plus riches (les objets du langage, etc.); avec les assistants de preuve on veut connecter des énoncés mathématiques dans les deux mondes, ce sont des types très très riches, et on veut des garanties d’interaction très fortes (préserver la correction mathématique).

D’une part, développer un assistant de preuve jusqu’à (1) qu’il devienne utilisable en pratique demande des efforts d’ingénierie importants, qui sont portés par des chercheurs (et étudiant-e-s en thèse, etc.). (2) C’est intéressant et important de se confronter à la pratique, mais cela tient aussi en partie du sacrifice : on prend sur son temps de recherche pour rendre service aux autres utilisateurs.

(1) Je pense que c’est justement dans la recherche que l’on peut se permettre d’avoir des outils qui ne finissent pas par être utilisable en pratique (et qui restent à l’état de jouets par exemple). Si l’on ne peut pas expérimenter de choses où l’on s’expose à un vrai risque que ça ne fonctionne pas en recherche, où pourrait-on le faire ? J’aurai tendance à dire que ce n’est pas parce que l’on appelle ça "ingénierie" que ça ne représente pas une part du travail de recherche, et pour compléter …

(2) Dans la même veine que l’enseignement, je pense que ce n’est pas seulement important, c’est vital pour la recherche. Il faut de temps à autre se rapprocher "du monde réel" justement pour ne pas s’enfermer dans une bulle de sûreté. Il faut montrer que l’utilisation de nos résultats est possible.

D’autre part, pour l’instant personne ne sait vraiment comment faire interopérer des preuves. […] Ça n’est pas un soucis pour des petits projets, mais aujourd’hui on commence à pouvoir et vouloir développer de vraies bibliothèques mathématiques contenant une partie importante des connaissances mathématiques, et le travail de redéveloppement pour chaque prouveur pourrait être colossal.

Justement, je ne pense pas que ça exclut d’expérimenter sur des systèmes autres qui seraient incomplets. Cela permet au moins de décortiquer les problèmes et d’en comprendre les points durs avant de les intégrer dans un gros système bien établi. Voir même de s’apercevoir qu’une partie de ce que sait faire notre "outil jouet" pourrait être intégré à un plus gros outil avec un vrai apport.

Il y a des gens qui travaillent sur comment relier les assistants de preuve entre eux, mais c’est un problème très difficile – pour les langages de programmation, les Foreign Function Interfaces marchent bien pour binder des procédures à des types/interfaces très simple, "prend un tableau de flottants et renvoie un entier", et nettement moins bien pour des types plus riches (les objets du langage, etc.); avec les assistants de preuve on veut connecter des énoncés mathématiques dans les deux mondes, ce sont des types très très riches, et on veut des garanties d’interaction très fortes (préserver la correction mathématique).

gasche

Peut être que des travaux comme ce qui tourne autour de Dedukti pourront nous sauver ^^ .

Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte