Intervention de Gilles Dowek

Il est beaucoup plus facile de développer des produits de qualité en utilisant des méthodes formelles au moment où on les développe, que de revenir sur des vieux codes d'il y a dix ou vingt ans, ou même de vieux algorithmes. En contrôle aérien, on m'avait demandé de démontrer la correction d'un algorithme ; je n'ai pas réussi et j'ai proposé mon propre algorithme. C'est de cette manière que l'on peut faire avancer les choses : davantage par une « co-conception » – conception de l'objet et de sa preuve en même temps – que par un retour sur le passé.

Ensuite, il ne suffit pas que les composants qui sont assemblés soient sûrs pour que l'ensemble le soit aussi. Mais les méthodes formelles peuvent s'appliquer aussi bien pour démontrer la sûreté de composants que celle de l'assemblage. Si cette dernière constitue un problème plus difficile, l'objectif est bien la sûreté globale, qui n'est jamais que celle du maillon le plus faible.