Résumé
Gilles Dowek, professeur à l’École Polytechnique, est l’auteur du livre « Les métamorphoses du calcul », Grand Prix de philosophie de l’Académie Française en 2007. Il a discuté les relations entre calcul et preuve, évidemment centrales pour la vérification des programmes. Il a montré que les algorithmes ont historiquement précédé les démonstrations, comme le prouvent de nombreuses tablettes d’argile de diverses origines, et que ces algorithmes étaient probablement prouvés corrects de façon non écrite. La notion de démonstration formelle a été introduite plus tard par les Grecs, probablement à partir d’algorithmes déjà existants ou inventés pour résoudre des problèmes précis, avant d’être développée pour son intérêt propre et de fonder les mathématiques. Des théorèmes bien connus comme Thalès et Pythagore correspondent effectivement à des problèmes algorithmiques. L’analyse de la preuve d’Euclide pour l’algorithme du calcul du pgcd par soustraction montre sa relation très étroite avec les méthodes modernes de preuves de programmes, qui s’intéressent bien sûr à des objets beaucoup plus gros, avec des démonstrations corrélativement beaucoup plus grosses qu’il est nécessaire de vérifier elles-mêmes par ordinateur.
