Griffonnages

Le Turing Award, c'est notre prix Nobel à nous, les informaticiens. Ça ne nous va pas si mal, dans le domaine, c'est vraiment la classe d'en avoir un. C'est pareil pour les matheux, chez eux la récompense suprême, c'est la médaille Fields. Comme ici ce n'est pas le Nouvel Obs, je ne vous dirai pas pourquoi il n'y aurait pas de prix Nobel en math.

Seulement voilà, sorti de la communauté, personne ne sait ce que c'est que le Turing Award, et ce n'est même pas médiatisé : pas un article dans le Monde, ni dans Libération, ni dans le Figaro.^[1] Et pourtant, le Turing Award 2007 a été décerné ce 4 février à Joseph Sifakis, un chercheur (franco)-hellénique, fondateur de verimag, un des laboratoires de recherche en informatique de Grenoble.

Il partage ce prix avec deux américains, E. Clarke et E. Emerson, pour leurs travaux sur le model checking.

Voici la vérité, je vous aurais bien entretenu du model checking, mais je n'y connais presque rien. J'ai fait un peu de googlage et tout, et quand j'ai vu qu'il y avait des modèles de Kripke, j'ai abandonné. Je garde des mes cours de logique (en licence) un souvenir confus : je ne me suis jamais bien entendu avec cette branche de l'informatique théorique. Et pourtant j'apprends que ça fait parti des cours de bases. Là, je m'étouffe.

Nous mettons là le doigt sur une spécificité de l'informatique théorique française, il y a une forte communauté de (pour faire simple) logiciens, et tous les dérivés : λ-μ-π-calculeurs, logisticiens exotiques (systèmes temporels, logique épistémique, etc...) et même des catégoriciens.

Leur graal, c'est d'arriver à comprendre ce qu'est un programme. Non, ne rigolez pas, ce n'est pas facile. Il faut dire que le passage de messieurs Curry et Howard a été déterminant : ils ont montré qu'un programme, c'est une preuve. Et de là découlent tout un tas de problématiques : un programme qui ne plante pas, c'est un démonstration juste. Et une démonstration juste, ce n'est rien d'autre que de la logique. Et les applications sont nombreuses : développement de nouveaux langages de programmation pour lesquels il est possible de certifier des propriétés de justesse sur le programme,^[2] assistants de preuves automatiques^[3], toute une panoplie de méthodes de vérification (dont le model checking fait parti). Ce sont ces gens là qu'il faut remercier pour avoir montré comment vérifier que les métros sans conducteurs ne font pas n'importe quoi.

Mais quand on lit ce qu'ils produisent, tout de suite, cela devient très abscons.

Cela donne un peu une vision à deux têtes à la recherche française en informatique théorique, groso modo, les logiciens d'un côté, les algorithmiciens de l'autre. Avec une douce guéguerre entre les deux. Par exemple, l'Université Paris 7 se retrouve avec deux labos : le LIAFA (Algo) et le PPS (Logique) et ceux qui passent par le MPRI (Master Parisien de Recherche en Informatique), master de recherche de Polytechnique, ÉNS Ulm & Cachan, P7) expliquent qu'ils ne connaissent qu'une seule moitié de la promo tellement le cloisonnement existe.

Donc, je suis heureux que cette prestigieuse récompense soit enfin décernée à un chercheur qui travaille dans un laboratoire français, je fais remarquer que c'est un chercheur au CNRS, ce qui montre combien cette institution est obsolète, et espère qu'un prochain Turing Award sera rapidement décerné à un algorithmicien français. Évidement, cela ne remet pas en question l'adage qui veut que les logiciens sombrent inéluctablement dans la folie.

Je vais finir par penser que le Turing Award, n'est pas l'agenda des medias. Si seulement il y avait un prix Nobel d'informatique ! Mais moi, à faire de l'informatique quantique, je pourrais toujours avoir un Nobel de physique en sus de mon Turing Award.