01 - Prouver les programmes : pourquoi, quand, comment ?

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Première leçon : La révolution informatique dans les sciences L'informatique sert depuis longtemps de moyen de calcul dans les autres sciences, que ce soit en sciences de la nature ou en mathématiques. Mais un changement profond de vison de son rôle dans les sciences naturelles est en cours : la pensée algorithmique et ses réalisations informatiques apportent désormais un regard nouveau sur la façon d'étudier les phénomènes, et cela en particulier dans les sciences de la vie qui n'ont été historiquement que peu touchées par les approches mathématiques. Les techniques de modélisation et de simulation, originellement dédiées à la simple imitation du réel, deviennent des outils conceptuels et pratiques fondamentaux pour comprendre les phénomènes concernés. Elle conduisent à une nouvelle vision algorithmique des lois de la nature, où l'information et son calcul servent à représenter de façon uniforme les objets classiques d'étude que sont la matière, les ondes et l'énergie. Cette vision est fondée sur de nouvelles mathématiques discrètes qui complètent les mathématiques continues habituelles et ouvrent de nouveaux champs d'action, en fournissant des schémas de raisonnement bien différents des schémas classiques. Nous illustrerons ce propos par des exemple pris aussi bien en physique, géophysique et astronomie qu'en biologie et médecine. Enfin, nous montrerons comment l'informatique moderne commence à transformer aussi les mathématiques, à travers la possibilité de conduire désormais des preuves vraiment formelles de très grande taille, réalisées en machine à l'aide de systèmes informatiques fondés sur des logiques formelles très puissantes qui seront étudiées dans la suite du cours.