du au

Le cours « Penser, modéliser et maîtriser le calcul informatique » a été donné dans le cadre de la chaire annuelle d’informatique et sciences numériques. Il a été le tout  cours de cette chaire, créée à la suite de mon cours précédent « Pourquoi et comment le monde devient numérique », lui-même donné en 2007-2008 dans le cadre de la chaire annuelle d’innovation technologique-Liliane Bettencourt. Le cours a été consacré à l’étude des fondements du calcul automatique, celui effectué par les ordinateurs petits ou grands présents dans tous les dispositifs numérisés, des méga-ordinateurs ou réseaux aux micro-puces embarquées dans les objets de toutes sortes. Comme je l’avais expliqué en 2007-2008, l’informatique est un art difficile si l’on veut faire la différence entre les applications qui marchent vraiment et celles qui marchent à peu près. Ces dernières se caractérisent par la présence de bugs résiduels induisant des comportements aberrants, avec des conséquences plus ou moins graves selon le type de système. Faire des applications qui marchent vraiment demande de raisonner sur les calculs qu’elles effectuent, à l’aide de modèles mathématiques, comme on raisonne sur des objets physiques.

Cependant, à cause de la taille et de la complexité des circuits et programmes, on s’aperçoit rapidement que le raisonnement sur papier ne suffit pas. Il faut introduire la notion clef de calcul sur le calcul, pour faire effectuer ou au moins vérifier les raisonnements par les machines elles-mêmes, en visant la vérification formelle automatique ou assistée de programmes et de circuits. Mais, pour pouvoir travailler ainsi, il faut d’abord formaliser la notion de calcul elle-même, ou plutôt les notions de calcul tant la discipline a progressé récemment.

Programme