En partenariat avec le séminaire “Codes Sources”
Institut de Mathématiques de Toulouse
Amphi Schwartz
17-18 septembre 2015
Jeudi 17 septembre, 14h-15h30, Damiano Mazza (CNRS, LIPN), « Voyage à travers les virus MS-DOS »
Entre la fin des années 1980 et la première moitié des années 1990, MS-DOS domine la scène des systèmes d’exploitation pour PC. Sa structure extrêmement simple, voire naïve, vis-à-vis de la gestion de la mémoire, des droits d’accès aux fichiers et des mesures de protection en générale (pratiquement inexistantes) fait de MS-DOS un terrain extraordinairement fertile pour le développement des virus informatiques dans le sens primordial (biologique) du terme : un morceau de code ne constituant pas en soi un programme mais s’appuyant à d’autres programmes pour s’exécuter et s’auto-répliquer, entraînant éventuellement des effets secondaires néfastes (la grande majorité de ce que l’on appelle « virus » informatiques aujourd’hui en effet ne le sont pas en ce sens).
Dans cet exposé, nous analyserons quelques exemplaires de ces organismes informatiques désormais éteints, en montrant leurs principes de fonctionnement et, pour certains, leur sophistication.
Jeudi 17 septembre, 15h45-17h15, Jacques Sauloy (IMT, Picard), « Le plus beau zoom du monde »
C’est un projet de fin d’année en « architecture » et « hard » sous la direction de Jean Conter qui avait une prédilection pour l’assembleur 68000 de Motorola. J’ai adoré l’assembleur 68000 et ce programme est, parmi ceux que j’ai écrits ces trente dernières années, l’un de mes deux ou trois préférés.
Vendredi 18 septembre, 10h30-12h, Baptiste Mélès (CNRS, AHP), « Spinoza en Coq : démonstration complète des premières propositions de l’Éthique »
L’Éthique de Spinoza est un traité philosophique écrit « à la manière des géomètres » : les théorèmes y sont démontrés à partir de définitions et d’axiomes initialement posés. Peut-on garantir la validité de démonstrations de Spinoza, et si oui, à quelles conditions ?
La tâche a été entreprise « à la main » par l’historien de la philosophie Martial Gueroult au tournant des années 1970. Pour emporter l’adhésion, ce travail devrait être vérifié ligne à ligne par un lecteur parfaitement rigoureux, hélas inexistant. Or depuis quelques décennies, les « assistants à la démonstration » tels que Coq sont des logiciels qui permettent de produire des démonstrations mathématiques complètes et certifiées. Nous présenterons donc la démonstration en Coq des premières propositions de l’Éthique de Spinoza.
Cette méthode présente un réel intérêt pour l’historien de la philosophie : elle permet non seulement de montrer certains détours « inutiles » dans les démonstrations de Spinoza, mais aussi de mettre au jour certains axiomes implicites de l’Éthique. Ces axiomes n’ayant métaphysiquement rien de trivial, on gagnerait à les expliciter. Par ce cas concret, on verra une fois de plus ce que les sciences formelles peuvent apporter à l’histoire « structurale » de la philosophie, qui, dans la lignée de Martial Gueroult et de Jules Vuillemin, travaille à reconstituer l’architecture interne des systèmes philosophiques.
Contact : Sébastien Maronne (IMT, Picard), smaronne@math.univ-toulouse.fr