De la logique avant toute chose : du programme de Hilbert à la naissance de la science informatique

«Wir müssen wissen ; wir werden wissen» («nous devons savoir ; nous saurons»).  C’est en ces mots que David Hilbert décrit, en 1930, l’ambitieux programme de recherche qu’il poursuit avec d’autres grands mathématiciens depuis le début du XXe siècle : refonder les mathématiques sur la base d’une logique qui soit cohérente, complète, et décidable.  Peu après, les résultats d’incomplétude de Gödel et d’indécidabilité de Church et Turing portent un coup fatal au programme de Hilbert.  Mais de cet échec émerge une belle théorie de la calculabilité, qui marque la naissance de la science informatique.  Après un retour sur ce grand moment de science, nous parlerons de l’extraordinaire impact qu’ont eu la machine de Turing et le lambda-calcul de Church (les deux formalismes introduits pour montrer l’existence d’énoncés indécidables) sur des sujets aussi variés que l’architecture des ordinateurs, la conception et la sémantique des langages de programmation, le célèbre problème P ≠ NP, et la démonstration mathématique assistée par ordinateur.