En France, nous avons des contacts avec l'équipe de Jean-François Monin au CNET de Lannion, qui explore depuis plusieurs années les différentes méthodes formelles applicables aux problèmes des opérateurs de télécommunication [31]. Ces contacts ont donné lieu à une CTI (consultation technique informelle) du CNET, en collaboration avec le projet Coq. Ceci nous a permis de financer la thèse d'Olivier Pons. Nous comptons poursuivre à l'avenir cette collaboration avec le CNET.
La RATP impose l'utilisation de méthodes formelles pour les logiciels qu'elle utilise pour contrôler les déplacements de ses véhicules, en insistant sur l'utilisation de la méthode B proposée par Jean-Raymond Abrial. Une entreprise de service installée à Aix, Digilog Stéria s'intéresse au développement d'un outil de spécification formelle, raffinement et production de code certifié suivant cette méthode, appelée ``Atelier B''. Les fondements logiques de la méthode B sont fondamentalement différents de ceux utilisés en Coq, puisqu'ils se restreignent à une théorie des ensembles fondées sur la logique du premier ordre. Néanmoins, il pourrait être possible de collaborer avec cette entreprise sur le thème des environnements de preuve.
La cryptographie est un domaine d'application privilégié pour les méthodes formelles. Pour l'instant les méthodes formelles ont été utilisées pour prouver des protocoles [14]. Nous avons engagé une réflexion avec le projet CODES pour comprendre comment la technique de certification que nous proposons pourrait s'appliquer aux briques de base de la cryptographie que sont les algorithmes de codage comme RSA (et ceux utilisés dans PGP par exemple).
Après les calculatrices et les langages de programmation structurée et typée, les systèmes de calcul formel ont fait leur entrée dans l'enseignement scientifique de premier cycle. Les systèmes permettant d'effectuer des démonstrations mathématiques vont les suivre logiquement, lorsqu'ils seront plus largement accessibles. Nous avons l'expérience depuis 3 ans de l'utilisation de Coq et CtCoq en maîtrise (Nice) et en DEA de mathématiques (MDFI). Comme on peut se passer de connaître et comprendre l'algorithme de Rish pour utiliser Maple, on peut aussi utiliser Coq sans connaître la théorie des types. Mieux, l'utilisation de Coq et CtCoq permet d'introduire par l'exemple les bases de la logique mathématique, qui ne sont pas enseignées comme telles, et que les étudiants apprennent (ou souvent n'apprennent pas) sur le tas.
Avec André Hirshowitz et Xiao Gang (Professeurs à l'Université de Nice-Sophia Antipolis, Laboratoire J. A. Dieudonné), et Frédérique Guilhot (Professeur agrégé en terminale), nous sommes convaincus que l'utilisation d'un système accessible de preuves formelles peut aider à montrer aux étudiants que les mathématiques élémentaires sont suffisamment simples et cohérentes pour être écrites et manipulées par une machine, qui d'habitude ne traite principalement que des nombres entiers, flottants ou des caractères. Cela peut aussi leur faire prendre conscience qu'une démonstration n'est pas une opération magique mais peut être décomposée en étapes simples selon des règles précises. Collaborer avec des enseignants devrait aussi nous permettre de confronter nos outils avec une large population d'utilisateurs novices, pour améliorer leurs fonctionnalités, leur ergonomie, etc.