Chaire Sciences du logiciel

Présentation

Écrire un petit programme informatique est facile. Concevoir et réaliser un logiciel complet qui soit fiable, pérenne et résistant aux attaques de sécurité reste extraordinairement difficile. C'est le but des sciences du logiciel que de concevoir et développer les principes, les formalismes mathématiques, les techniques empiriques et les outils informatiques nécessaires pour concevoir, programmer et vérifier des logiciels fiables.

L'enseignement de la chaire Sciences du logiciel vise à explorer cette problématique et à présenter la recherche contemporaine dans ce domaine. Le cours privilégie les approches dites « formelles », par opposition à l'empirisme souvent de mise en génie logiciel. Ces approches s'appuient sur des fondements mathématiquement rigoureuses, connues ou en émergence : sémantiques formelles, logiques de programmes, systèmes déductifs, équivalences de programmes, calculs de processus... Historiquement, ces concepts ont émergé de considérations de programmation très terre-à-terre avant de se parer de rigueur mathématique. Le cours s'efforce de retracer ce cheminement des idées en partant de l'intuition du programmeur. Une autre question récurrente dans le cours est la mécanisation de ces approches formelles : comment s'aider de la puissance de la machine pour automatiser, en tout ou en partie, leur application ?

Les premières années de cet enseignement pourraient s'intituler « Programmer, démontrer », car ils explorent plusieurs modes d'interaction entre la programmation de logiciels et la démonstration d'énoncés mathématiques. Programmer puis démontrer, c'est l'approche désormais entrée dans la pratique de vérification formelle a posteriori d'un logiciel déjà écrit, à l'aide de logiques de programmes et d'analyses statiques. Programmer pour démontrer, c'est l'approche plus futuriste de la synthèse de programmes corrects par construction ; mais c'est aussi la démarche suivie par des logiques constructives comme la théorie intuitionniste des types et par des assistants à la démonstration comme Coq et Agda. Enfin, programmer égale démontrer, c'est la célèbre correspondance de Curry-Howard, objet de la première année du cours, qui met en relation de manière extraordinairement féconde des logiques mathématiques et des langages de programmation fonctionnels typés comme OCaml et Haskell.