Aujourd’hui, réveil à 10h. C’est un peu tard mais tant pis, les bureaux ne ferment de toute façon pas avant 20h. Après avoir failli me faire renverser deux fois à cause du nombre indécent de voitures en ville et de l’horrible aménagement urbain, j’arrive au bureau sans objectif clair pour la journée.
Je pourrais lire un papier de recherche, essayer d’avancer la théorie développée dans ma thèse, ou encore continuer le prototype montrant la faisabilité de cette théorie. Ces possibilités ont toutes le même objectif, celui que j’ai depuis deux ans, qui est de créer un logiciel qui prouve que d’autres logiciels sont corrects.
Pourquoi faire ? Comme d’habitude : pour automatiser une tâche que l’on sait faire manuellement mais péniblement.
S’ensuit la question que les gens me posent habituellement et dont la version clarifiée est : Ça veut dire quoi « prouver un logiciel » ? N’a-t-il pas été écrit pas un expert qui savait ce qu’il faisait, et ensuite testé ?
Eh bien si, enfin parfois, mais c’est insuffisant.
Prouver qu’un logiciel est correct, c’est s’assurer qu’il se comportera toujours comme prévu. Il y a deux mots intéressants ici.
« prévu » , déjà, ce qui signifie qu’il faut avoir une idée très claire de ce qu’il est censé faire. Si claire qu’on doit pouvoir le faire comprendre à l’ordinateur.
Le second mot intéressant est « toujours » , et celui-là est plus compliqué.
De la même manière qu’on ne peut pas faire confiance au menu indiqué dans notre restaurant universitaire dans les situations exceptionnelles, par exemple quand on y va comme aujourd’hui après 13h, on ne va pas non plus pouvoir faire confiance à un logiciel qui s’exécute sur un ordinateur qui brûle. « toujours » se comprend donc à un certain niveau d’abstraction sur la réalité, en supposant que certaines choses basiques se déroulent parfaitement. Une fois ce niveau d’abstraction fixé, on peut commencer à prouver formellement que le logiciel se comporte comme prévu.
Bien que l’idée soit la même, celle de convaincre, il ne faut pas confondre l’usage formel et familier du mot « preuve ».
La preuve formelle est un argument irréfutable et pas trop dur à vérifier, ici en faveur du fait que le logiciel fonctionne comme prévu.
L’avantage de l’irréfutabilité de la preuve est qu’il n’est pas nécessaire d’en accumuler ; une preuve, n’importe laquelle, nous suffit à être certains que le logiciel est correct.
Mon rôle est donc de concevoir un logiciel qui, pour n’importe quel logiciel et comportement énoncé à son propos, essaie de trouver une preuve de sa véracité ou fausseté. C’est une tâche impossible (théorème de Rice), mais essayer de s’en approcher est utile aussi.
Ce sera pour un autre jour : il est 20h20 et un vigile qui passe dans les bureaux me propose de partir.
