Séminaire « Codes sources »
L'objectif du séminaire Codes sources est de présenter la pensée informatique là où elle s'exprime le plus concrètement : dans les textes que sont les codes sources. Séance du jeudi 7 février 2019 (14h-16h) : Assia Mahboubi (Inria, LS2N, Université de Nantes) : « Démonstrations assistées par ordinateur » Résumé : Les ordinateurs ont profondément transformé la pratique des mathématiques contemporaines, mettant en particulier leur puissance de calcul au service de l'observation, de la conjecture et même de la validation "par calcul". La généralisation rapide de l'accès à une puissance de calcul surhumaine a même suscité de nouvelles formes de mathématiques, à l'interface avec l'informatique, comme le calcul formel ou l'analyse numérique. Moins connus que certains systèmes de calcul symbolique, numérique ou statistique, les "assistants de preuve" font néanmoins partie des logiciels qui permettent de faire des mathématiques sur ordinateur. Ils sont conçus pour aider leurs utilisateurs à représenter définitions, énoncés et démonstrations dans un formalisme logique précis et non ambigu, sous la forme de bibliothèques digitales de mathématiques formalisées. Il existe plusieurs sous-familles d'assistants de preuves, qui diffèrent en particulier sur le choix de fondations logiques, qui détermine le langage formel utilisé. En particulier, une majorité d'entre eux sont basés sur une forme de théorie des types, une approche des fondations logiques qui donne une place privilégiée aux fonctions, et au concept de calcul. Mais dans tous les case, une telle (ré)écriture des théories mathématiques serait bien trop piétonne pour être envisageable, sinon intéressante, sans l'aide de la machine. Cette dernière permet en retour de réduire la vérification des preuves à une tâche routinière et mécanisée. Mais ce n'est pas le seul bénéfice d'une telle formalisation et nous discuterons dans cet exposé la pratique et les enjeux de cette forme de mathématiques assistées par ordinateur. Cet exposé ne présuppose pas de connaissance particulière en logique ou en programmation. Lieu : Salle 24-25/405 du LIP6 (rotonde 25, 4e étage) Adresse : 4 place Jussieu, 75005 Paris métro Jussieu (lignes 7 et 10) ------------------------------------------------------------------------ Prochaines séances du séminaire Codes sources : - Jeudi 28 mars 2019 : Bastien GUERRY, « Code source et/ou documentation ? Réflexions autour de l’éditeur Emacs, du langage Emacs Lisp et du module Org-mode » - Jeudi 11 avril 2019 : Marie-José DURAND-RICHARD (Paris 8, SPHERE), « Les diagrammes de fonctionnement de The Analytical Engine, de Charles Babbage 1791-1877) à Ada Lovelace (1815-1852) » - Jeudi 23 mai 2019 : à déterminer - Jeudi 13 juin 2019 : à déterminer Sauf mention contraire, toutes les séances ont lieu de 14 heures à 16 heures au LIP6. ------------------------------------------------------------------------ /* *************************************** * À propos du séminaire Codes sources * *************************************** */ À celui seul qui prend la peine de les lire effectivement, les codes sources révèlent leur richesse. On y découvre que l'élégance d'un algorithme réside parfois hors de sa complexité, dans l'usage virtuose des idiomes du langage de programmation ou dans la connaissance fine de la machine à laquelle il est destiné. Bien souvent des codes sources comportent davantage de lignes de commentaires que de code. Tous ces trésors de pensée informatique fondent à la compilation comme neige au soleil — preuve qu'un programme n'est pas seulement écrit pour être compilé. Le but du séminaire est de décrire ces œuvres de l'esprit comme des textes à part entière. Nous espérons ainsi contribuer à la constitution d'une culture générale en programmation. En informatique comme en littérature, cela suppose la familiarisation progressive avec un corpus de grands textes. À chaque séance, un intervenant — jeune chercheur ou chercheur confirmé en informatique, en histoire ou en philosophie — présente, en moins d'une heure, un code source de son choix : un fragment de système d'exploitation, de pilote, de compilateur, de bibliothèque... Le code peut avoir été écrit par l'orateur ou par quelqu'un d'autre, dans quelque langage que ce soit. Le commentaire peut être algorithmique, stylistique, historique ou philosophique, et porter sur tous les aspects du code, commentaires compris. Le code est ensuite discuté avec l'auditoire. Organisateurs : - Raphaël Fournier (CNAM) - Baptiste Mélès (CNRS, Archives Henri-Poincaré) - Lionel Tabourier (LIP6). Site : http://codesource.hypotheses.org/ Contact : Baptiste Mélès ([email protected]) Twitter : https://twitter.com/SemCodesSources Liste de diffusion : https://groups.google.com/forum/#!forum/codes-sources ------------------------------------------------------------------------ -- Baptiste Mélès Chargé de recherche au CNRS (CNRS Researcher) Archives Henri-Poincaré—Philosophie et Recherches sur les Sciences et les Technologies (CNRS UMR 7117, http://poincare.univ-lorraine.fr) Université de Lorraine — Université de Strasbourg /Philosophia Scientiæ/ (Rédacteur en chef adjoint / Managing editor) https://journals.openedition.org/philosophiascientiae/ 91 avenue de la Libération, 54000 Nancy, France http://baptiste.meles.free.fr/ -- Pour toute question, la FAQ de la liste se trouve ici: https://www.vidal-rosset.net/
