Nous nous inscrivons dans une tendance de l'informatique et du calcul scientifique dont le but est d'obtenir une fiabilité meilleure des programmes d'ordinateurs, et dont les méthodes sont fondamentalement mathématiques. Ces méthodes, qu'on appelle ``méthodes formelles'', ont la particularité d'intervenir très tôt dans le processus de création des programmes, contrairement aux méthodes de validation à posteriori (tests) qui prévalent encore. Les programmes sont considérés comme des objets mathématiques comme les autres, ce qui a l'avantage de permettre de décrire clairement, sinon sans ambiguité, leurs comportements (jusqu'au niveau de l'implémentation), et d'effectuer des raisonnements et des preuves sur leurs propriétés. L'utilité des méthodes formelles commence à être reconnue par les industriels pour qui l'absence de bogue dans les programmes est vitale (avionique, télécom, circuits intégrés). Mais la production de programmes sans bugs n'est pas la seule utilité de ces méthodes. Elles permettent aussi de contrôler le développement de logiciels modulaires, en permettant d'isoler et de spécifier clairement les composants élémentaires. L'agencement de ces composants étant lui-même susceptible d'être étudié par les même méthodes (protocoles de communication par exemple).
Pour ce qui nous concerne, le domaine qui retient notre attention est celui du calcul scientifique. Il a deux caractéristiques. La première est qu'il fait intervenir des algorithmes mathématiques sophistiqués. La deuxième est son exigence de rapidité d'exécution.
Il est très difficile de vérifier autrement que par des tests poussés (simulation) un code de calcul scientifique. Pour deux raisons: la première est la taille de son implémentation, la seconde la complexité des algorithmes qu'il met en oeuvre. Ce sont autant de sources d'erreurs. Les erreurs d'implémentation peuvent être corrigées par des techniques d'analyse de programme (bornes dans les indices de tableaux, initialisations de variables, etc), mais les erreurs dans les algorithmes (cas limites, cas dégénérés, ou pire) ne sont pas accessibles par des techniques traditionnelles. Le seul moyen de les détecter et de les corriger est d'effectuer des démonstrations mathématiques détaillées et exhaustives, qui sont fatalement lourdes et fastidieuses si on ne dispose pas d'outils et d'environnement adapté pour les effectuer.
C'est précisément une des caractéristiques du domaine des méthodes formelles que de chercher à augmenter la puissance et la productivité des processus de conception et de vérification de programmes complexes, en permettant au programmeur d'exprimer son programme et spécifications dans un langage formel de haut niveau, dont la traduction en langage machine (compilation) sera transparente et sûre (extraction de programmes, compilateur certifié). C'est aussi grâce à cela qu'elles sont utiles et le seront de plus en plus.
Les utilisateurs que nous visons sont variés, mais on peut les grouper dans trois catégories.
Il existe une catégorie d'utilisateurs industriels qui se démarque de la communauté Coq. En effet, il existe plusieurs grands industriels qui cherchent à augmenter l'utilisation de méthodes formelles dans leur processus d'ingéniérie: Aérospatiale, Dassault, Matra Transports, Alcatel, Bull. Ces industriels font appel à des sociétés externes pour leur fournir des environnements de travail pour leur ingénieurs. Il existe donc un secteur naissant de sociétés dont l'objectif est de fournir des solutions de développement à base de méthodes formelles, par exempl les sociétés Verilog, Steria, Logica (U.K). Pour utiliser efficacement les méthodes formelles dans le développement de logiciel, il est nécessaire d'avoir des outils permettant de traiter ensemble les programmes, leurs spécifications, et les documentations et de vérifier mécaniquement la cohérence de tous ces documents. En nous concentrant sur le système Coq nous développons les compétences nécessaires à la mise au point de tels outils, compétences qui intéresseront certainement tous les intervenant du secteur naissant des fournisseurs d'outils pour les méthodes formelles.
Pour ce qui concerne l'utilisation d'implantations certifiées, on a en vue deux exemples.
La société Prover Technology (Suède), a spontanément manifesté son intérêt pour l'implantation certifiée de l'algorithme de Stallmark effectuée durant le stage de Pierre Letouzey, nous donnant une licence d'utilisation de son logiciel (implémentant cet algorithme). Avec une implantation plus efficace, sur laquelle travaille Laurent Théry (preuves de mémoires), on peut espérer une expérience d'utilisation de code certifié par cette société.
Enfin, une version certifiée de l'algorithme RSA est en fin de développement (G.Barthes et un collègue portugais), qui devrait nous servir d'argument dans les contacts que nous avons avec le projet Codes et que nous espérons nouer avec une société développant du code cryptographique.
Avec des enseignants de Nice (A.Hirshowitz, G.Xiao, F.Guilhot), nous réfléchissons à l'utilisation d'outils de démonstration comme CtCoq et Coq dans l'enseignement des mathématiques en premier cycle. L'objectif est d'utiliser une version adpatée de CtCoq (via le Web) dans les TD du cours d'algèbre l'année prochaine (99-2000) en DEUG 1ère année. On essaiera d'intégrer le serveur Wims d'exercices interactifs de mathématiques développé par G.Xiao. On peut relier cette approche avec ce qui passe dans l'enseignement avec Maple (classes prépa, université): le calcul mathématique est maintenant enseigné avec des outils informatiques. Notre but est que le raisonnement mathématique suive le même chemin.
Les utilisateurs seront alors très nombreux (étudiants), et exigeants (enseignants). C'est une sorte de défi que nous souhaitons relever, d'autant plus que la concurrence est sporadique, et inexistante à notre connaissance en France (parmi les autres efforts pour fournir des outils d'enseignement de la logique mathématique en classe, on peut citer Jape en Angleterre et Imps aux USA).
A coté de ces trois classes d'utilisateurs, il serait bon d'avoir des aventures avec nos collègues du calcul scientifique/formel/geometrique (stages de DEA co-encadrés) portant sur des points particuliers (algorithmes à prouver, implémentation à tester, support d'enseignement).