Ours & Hippy — le blog

Comme rz0 l’a admirablement fait remarquer, le blog est plutôt mort ces temps-ci. Sans surprises, je suis occupé depuis le début de l’année, et le temps pour poster des billets en a diminué d’autant. Je me suis fixé l’objectif de ne pas passer plus d’une heure à écrire ce billet (écriture seulement, il y aura sans doute de la relecture ensuite), et ça me paraît un pari assez raisonnable, bien que nettement plus ambitieux que les billets précédents. La qualité en souffrira certainement, mais j’essaie de trouver un équilibre.

Je remarque d’ailleurs que je ne suis pas le seul à être occupé : tous ces gens qui avaient promis juré que oui, ils feraient des efforts pour poster des commentaires de temps en temps, histoire qu’on conserve la motivation, ils ont visiblement un travail fou. Tant pis ; de toute façon je n’ai pas les moyens (temps, motivation et envie) d’écrire de gros billets bien préparés en ce moment. Si j’écris celui-ci, c’est parce que j’ai honte de laisser cet espace tellement vide alors que rz0 a fait tant d’effort pour m’installer un petit coin bien douillet. Et j’espère aussi que ce que j’ai à vous raconter pourrait vous intéresser.

Débuts en Coq

Cette année, j’ai décidé de me lancer dans le vaste monde des assistants de preuve. En un mot, ce sont des programmes qui permettent d’écrire des preuves mathématiques, et qui les valident : ils savent dire si oui ou non, une preuve est correcte.

Je leur vois deux intérêts principaux. D’une part, ils permettent de se redonner confiance en mathématiques ; si vous connaissez le malaise de celui qui écrit un brouillon de preuve, mais sans savoir vraiment si elle est juste ou contient une erreur désagréable que vous n’aviez pas vue, vous comprendrez ce que je veux dire. Plus généralement, c’est un peu comme la différence, en informatique, entre écrire du pseudo-code, et écrire dans un vrai langage de programmation : l’avantage d’un vrai langage, c’est que vous pouvez exécuter le programme pour vérifier qu’il fonctionne (et en particulier vérifier sa syntaxe, etc. automatiquement), alors qu’on est rarement motivé pour relire avec soin un pseudo-code. L’ordinateur apporte un retour d’expérience (feedback) direct, impartial et incontestable.

D’autre part, les assistants de preuve sont essentiellement des langages de programmation. Ils se placent en effet à cheval entre la théorie des types (côté informatique) et la théorie de la démonstration (côté mathématiques) : c’est essentiellement le même domaine, vu de points de vue différents. On parle souvent de l’isomorphisme de Curry-Howard, mais ce théorème précis concerne des systèmes bien précis, et l’étendue de la correspondance est en fait beaucoup plus large ; fondamentalement, depuis le début du 20e siècle, on pense les preuves formelles comme des programmes (fonctionnels). Ces outils font donc de bons mélanges entre des preuves très formelles et des langages très fortement typés, et ça a tout pour me plaire. On peut d’ailleurs aussi utiliser ces systèmes pour prouver des choses sur les langages de programmation (tous paradigmes confondus, cette fois-ci).

Il existe plusieurs systèmes d’assistants à la démonstration. Les plus utilisés actuellement sont Coq et Isabelle (et éventuellement Twelf et HOL-Light, avec aussi des anciens couverts de lauriers (Mizar), et de jeunes qui explorent l’espace de recherche (Agda)). Ces systèmes ont des qualités et des défauts variés. J’utilise Coq. D’une part parce que c’est le système conçu en France, et donc je suis entouré de gens qui l’utilisent, l’enseignent, voire le développent.^α D’autre part, j’utilise pour apprendre les bases le livre en ligne Certified Programming with Dependent Types, qui conseille d’utiliser Coq et qui a certainement ses raisons, moi, je ne connais pas assez le domaine pour faire un choix informé.

Ces outils sont majoritairement codés dans un des langages dont le nom contient « ML » et ne commence pas par « X ». C’est une corrélation historique, puisque le langage ML (notre grand-père à tous) a été créé conjointement à l’assistant de preuve LCF.

Au passage, si vous envisagez vous-même de vous intéresser un jour au sujet, je suis assez content de ce bouquin. En particulier, il prend surtout ses exemples dans le monde des langages de programmation : dès le premier chapitre, on compile des expressions arithmétiques simples vers une machine à pile simple, en rajoutant du typage à gogo, et sera donc plus accessible qu’un livre orienté vers la logique formelle si vous vous sentez plutôt informaticien. Une connaissance (au moins des bases) de la programmation fonctionnelle est tout de même indispensable.

Il est temps de signaler les deux articles qu’asmanur a écrit comme une petite introduction à Coq (un passe-temps qu’il a certainement abandonné assez vite, comme tous les autres) : Voyage au bout de la logique, et sa deuxième partie. Si vous vous intéressez à la discussion sur le choix de l’assistant à la démonstration, vous pouvez aussi lire l’introduction du livre de Chiplala. Au passage, le mode Emacs qu’il recommande, Proof General, est vraiment très bien.

Programmation par contraintes

Cette fois-ci, cela tient plus de l’anecdote, mais je trouve ça assez amusant pour avoir envie de vous en parler. En plus de la logique formelle fonctionnelle typée et des hautes sphères éthérées de la théorie des catégories, je fais cette année des choses bassement matérielles qui demandent de la programmation. Évidemment, je fais tout en OCaml.

Depuis cet été, je suis assez séduit par les types fantômes. C’est un outil vraiment puissant et agréable, à tel point que je suis tenté d’en mettre un peu partout dans mes divers projets. Par exemple, je dois coder un projet de bataille navale en réseau (et d’ailleurs c’est assez ennuyeux ; je prends sur mon temps de développement pour vous écrire cet article). Ça a l’air assez trivial, mais j’ai perdu tellement de temps à refactoriser dans tous les sens pour avoir le typage le plus expressif possible que j’en suis venu à m’auto-imposer la règle suivante : « Interdiction d’utiliser les types fantômes ! »

Et vous, avez-vous des règles personnelles que vous appliquez avec cruauté, pour éviter de perdre votre temps dans des considérations, certes intéressantes, mais déraisonnables pour le projet précis sur lequel vous travaillez ?

J’en profite pour vous signaler que j’étais passé à côté jusqu’à présent, mais j’ai découvert récemment que la bibliothèque standard OCaml utilise elle aussi, des types fantômes, ma bonne dame : ça se passe dans le module le plus haut niveau de la bibliothèque, Bigarray.

Traitement d’images

Je suis, par un curieux hasard de circonstances, un cours de traitement d’images. C’est un sujet très éloigné de mes centres d’intérêt habituels, mais je ne le regrette pas. Je vois défiler beaucoup de jolies photos, et de méthodes pour les améliorer encore, parfois franchement inventives. J’ai un professeur formidable, qui est un mordu de la photographie, mais aussi un amateur de l’analyse de Fourier. Sans entrer dans les détails pénibles, il nous fait des démonstrations « avec les mains » qui sont parfois assez sympathiques, et donnent un petit coup de jeune à toutes ces choses qui sombrent lentement dans l’oubli quand on ne les utilise pas.

Au cas où ça vous intéresse, voici un exemple d’algorithme que nous avons étudié : Colorization Using Optimization. Il s’agit de donner des couleurs à des images en noir et blanc, à partir de quelques indications de l’utilisateur (des traits de couleur connue). L’idée de base, c’est de supposer que deux pixels de luminosité proche doivent être de couleur proche. On peut alors exprimer la teinte de chaque pixel en fonction de celle de ses voisins et, combiné aux conditions initiales de l’utilisateur, ça donne un gros système linéaire (une grosse matrice) qu’on fournit à une fonction de résolution et pouf, une image en couleur. Ça marche étonnamment bien.

Pour ce cours, j’ai participé à l’écriture de bindings OCaml vers des bibliothèques C (ou interfacées par l’intermédiaire du C), par exemple OpenCV ou SuiteSparse. C’est très drôle, on retrouve la joie du segfault (et c’est encore mieux à plusieurs). Je ne m’étais jamais vraiment plongé dans l’interface C-OCaml, et je peux vous dire que ce n’est pas inoubliable mais ça reste une expérience amusante. Cela m’a d’ailleurs permis de mettre mon petit grain de sel dans un tutoriel de Cacophrène à ce sujet sur le SdZ. Ça fait toujours une introduction en français à ce sujet, qui peut servir de mise en bouche, mais si un jour vous voulez vraiment coder quelque chose je vous conseille ensuite de lire conjointement le manuel officiel pour les idées, et le tutorial en anglais de François Monnier pour les exemples de code. Attention au DA-Ocaml, sur ce point il est un peu vieux.

Une petite réaction pour finir ?

Que serait mon billet mensuel sans une référence, ou du moins une allusion, à un petit papier à se mettre sous la dent ? J’en ai survolé une bonne poignée depuis la rentrée, mais les derniers que j’ai croisés sont des articles de Gilad Bracha. C’est un type qui a commencé ses exploits en codant un système Smalltalk avec annotations optionnelles de typage très performant^γ, pour aller ensuite réutiliser ses compétences en travaillant sur Java, sa spécification et sa VM chez Sun pendant quelques temps, avant de repartir construire un nouveau langage dynamique, Newspeak.

J’ai jeté un coup d’oeil à la bête. Comme vous imaginez, les langages très dynamiques ne sont pas forcément ceux qui me tentent le plus, mais ça fait du bien de voir ce qui se fait ailleurs de temps en temps. J’ai aussi lu deux de ses papiers au hasard : Executable Grammars in Newspeak, et Pluggable Type Systems.

Le premier papier présente une façon possible de créer une bibliothèque de parsing combinators dans un langage dynamique. Comme l’annonce l’auteur d’entrée de jeu, c’est plutôt le point fort des langages fonctionnels (l’étalon dans le domaine étant le très bon Parsec de Haskell). Il promet que les fonctionnalités nouvelles de son langage, ainsi que son fort dynamisme, permettront d’en faire une traduction « objet dynamique » adaptée. Je n’ai pas été émerveillé par le résultat (en particulier, comme toutes les approches « DSL internes au langage », la syntaxe n’est au final pas si géniale que ça), mais ça reste une lecture intéressante. Il discute aussi de la facilité ou non à typer ces opérations dans un langage statique, mais le référentiel semblant être celui de Java, on en apprend plus sur l’état des systèmes de types mainstream que sur le fond du problème.

Le deuxième article n’est pas vraiment un article scientifique, mais plutôt une prise de position de l’auteur. Il voudrait qu’on envisage les systèmes de type non pas comme une donnée fondamentale du langage de programmation, à laquelle tout programme dans ce langage doit se soumettre, mais comme une étape supplémentaire, optionnelle. C’est une idée très séduisante, mais assez délicate à mettre en place en pratique (la plupart des avantages théoriques des systèmes de types actuels venant justement de leur capacité à (presque) tout contrôler).

Il voudrait aussi que l’inférence soit optionnelle/désactivable, en un mot « pluggable », ce qui est un point de vue intéressant (et trouve des échos chez les théoriciens^δ). Il voudrait même pouvoir faire cohabiter plusieurs systèmes d’inférence pour « choisir le meilleur selon les situations », et là je ne suis franchement pas convaincu : ça mène à une situation où le type repose sur beaucoup d’heuristiques diverses que le programmeur ne maîtrise pas en général, et cela pourrait à mon avis poser plus de problèmes que ça n’en résoud. Ça reste une lecture intéressante, c’est agréable de voir que les universitaires grisonnants ne sont pas les seuls à se poser la question.

Pour amadouer mes lecteurs potentiels les plus revêches, je dois signaler que cet article cite explicitement les essais d’ajout (partiel) d’un typage statique au langage Erlang.

P.S. : Mon pari de temps n’a pas été tenu, j’ai plutôt mis une heure et demie, mais c’est toujours agréable d’écrire. Ma bataille navale avance assez bien : les clients peuvent se connecter, lancer des parties et placer leurs bateaux, et je vais bientôt être obligé de coder la partie où ils tirent les uns sur les autres. Heureusement, j’ai glissé des variantes polymorphes pour que le type des fonctions reflète le protocole de communication.