Ceux de mes lecteurs qui ont eu la curiosité de se pencher sur mes sujets de recherche savent que je fais de l'analyse statique de programmes ; je renvoie par exemple à l'introduction de mon mémoire d'habilitation à diriger les recherches pour une présentation générale de la problématique du sujet.

Dans ce domaine, j'ai travaillé à la fois sur des aspects théoriques (voir par exemple mon récent article avec Thomas Gawlitza mêlant théorie de la complexité, théorie des jeux et analyse statique) et sur des aspects pratiques : j'ai notamment participé au développement de l'outil Astrée, actuellement commercialisé par la société Absint.

J'envisage le développement d'un autre outil. Se pose notamment la question de la base permettant l'entrée des programmes dans l'outil, et d'un éventuel langage intermédiaire.

  1. Dans Astrée, j'avais écrit, avec mes collègues, un début de compilateur C (analyse lexicale et syntaxique, typage).

  2. Mon étudiant Julien Henry part du bitcode LLVM. Des collègues me disent que c'est leur choix également.

  3. Mon collègue Jean-Christophe Filliâtre me propose le langage intermédiaire de son outil Why.

  4. Mon collègue Francesco Logozzo me vante les vertus du code .NET.

  5. Ma collègue Laure Gonnord me dit du bien de l'infrastructure Rose.

  6. Mon collègue Joshua Berdine me conseille de partir du code source C avec mon propre début de compilateur.

  7. D'autres collègues de Microsoft me vantent le langage Boogie de mon collègue Rustan Leino.

  8. Mon collègue Viktor Kuncak essaye de faire converger le projet RichModels.org. Pour le moment, ils parlent d'un sous-ensemble du langage de l'assistant de preuve Isabelle.

  9. Un collègue rencontré à CGO, pourtant expert en GCC, m'a conseillé de me brancher dans Clang, le compilateur C/C++ de LLVM, mais à un niveau supérieur au bitcode.

  10. Mes collègues de Saclay me conseillent de me brancher dans leur outil Frama-C.

  11. Mon collègue Radu Iosif propose son propre langage intermédiaire sur les scalaires et les tableaux.

  12. Mes collègues de la NASA font leur propre langage intermédiaire, en partant de la LLVM.Constatez la diversité des points de vue. Ensuite, se pose la question du langage d'implémentation : les uns sont en Caml, d'autres en C# voire F#, d'autres en Scala, d'autres ne jurent que par C++...

Constatez la diversité des points de vue. Ensuite, se pose la question du langage d'implémentation : les uns sont en Caml, d'autres en C# voire F#, d'autres en Scala, d'autres ne jurent que par C++...

Je suis perplexe.

(PS : Oui, il ne s'agit pas de problèmes scientifiques, mais de problèmes d'ingéniérie... Pourtant, un mauvais choix d'ingéniérie, et les expérimentations deviennent bien plus difficiles... Qui plus est, si la représentation intermédiaire utilisée est de trop bas niveau, il va falloir reconstruire la vision de plus haut niveau, ce qui peut poser des problèmes scientifiques non triviaux.)