[ATHENA] Séminaire Codes Sources : Démonstrations assistées par ordinateur (Assia Mahboubi, 7 février 2019)

[Baptiste Mélès <baptiste.meles AT gmail.com>]

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 (baptiste.meles AT univ-lorraine.fr)

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/