Journal Nouvelle chaire Sciences du logiciel au Collège de France.

Posté par  . Licence CC By‑SA.
Étiquettes :
41
14
nov.
2018

À partir de cette année l'informatique et les sciences du numériques se voient dotées d'une nouvelle chaire au Collège de France, intitulée « Sciences du logiciel », dont le titulaire est Xavier Leroy. Xavier Leroy est connu pour être l'architecte et un des principaux développeurs du langage de programmation fonctionnel OCaml ainsi que du compilateur C formellement vérifié CompCert. Il a reçu en 2016 le prix Milner pour récompenser ses travaux sur la fiabilité des systèmes informatiques.

La leçon inaugurale de cette nouvelle chaire aura lieu demain à 18h00, sera diffusée en direct via le site du Collège de France et aura pour thème « Le logiciel, entre l'esprit et la matière ».

Les leçons de cette année se tiendront le mercredi matin à 10h00 dès la semaine prochaine sur le thème « Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui » (programme de l'année). Usuellement, les cours sont disponibles en streaming ou en téléchargement une semaine après sur la page dédiée. Le cours est présenté en ces termes sur le site du Collège de France :

Informatique et logique mathématique sont historiquement liées : Alan Turing, John von Neumann, Alonzo Church et bien d’autres fondateurs de l’informatique étaient logiciens, professionnels ou de formation. Le cours 2018-2019 de la chaire de Sciences du logiciel étudie un autre lien, de nature mathématique celui-là (il s’agit d’un isomorphisme), entre langages de programmation et logiques mathématiques. Dans cette approche, démontrer un théorème, c’est la même chose que d’écrire un programme ; énoncer le théorème, c’est la même chose que de spécifier partiellement un programme en donnant le type qu’il doit avoir. […]

Le cours retracera ce bouillonnement d’idées à la frontière entre logique et informatique, et mettra l’accent sur les résultats récents et les problèmes ouverts dans ce domaine. Le séminaire donnera la parole à 7 experts du domaine pour des approfondissements et des points de vue complémentaires.

Pour ma part, une leçon a particulièrement retenu mon attention, celle du 9 janvier : Le forcing, une transformation de programme comme une autre ? Le forcing, pour ceux qui ne connaissent pas, est une technique de démonstration inventée dans les années 1960 par Paul Cohen pour prouver l'indécidabilité de certains énoncés en théorie axiomatique des ensembles, comme l'hypothèse du continu de Cantor.

  • # "chaire"

    Posté par  (site web personnel) . Évalué à 2.

    Une nouvelle quoi?

    • [^] # Re: "chaire"

      Posté par  . Évalué à 4. Dernière modification le 14 novembre 2018 à 23:05.

    • [^] # Re: "chaire"

      Posté par  . Évalué à 6.

      De la chaire fraîche !

      "Quand certains râlent contre systemd, d'autres s'attaquent aux vrais problèmes." (merci Sinma !)

    • [^] # Re: "chaire"

      Posté par  (Mastodon) . Évalué à 2.

      Une chaire célèbre est celle des math à l'université de Cambridge. Vu la tartine de célébrités qui y sont passées, tu imagines l'honneur de celui qui la tient actuellement : Isaac Newton (ne serait-ce que pour lui d'ailleurs), Charles Babbage, Paul Dirac, Stephen Hawking…

      En théorie, la théorie et la pratique c'est pareil. En pratique c'est pas vrai.

  • # Un peu de finesse ...

    Posté par  . Évalué à 3.

    Merci pour cette bonne nouvelle. Un peu de finesse dans notre monde de brut fait du bien.

  • # Collège de France

    Posté par  (Mastodon) . Évalué à 10. Dernière modification le 15 novembre 2018 à 08:10.

    Moi c'est le Collège de France que je ne connaissais pas (même si je connaissais de nom), et ce truc est tout simplement génial.

    Extrait de la page Wikipedia :

    Le Collège de France, anciennement nommé Collège royal, […] est un grand établissement d'enseignement et de recherche. Il dispense des cours non diplômants de haut niveau dans des disciplines scientifiques, littéraires et artistiques. L'enseignement y est gratuit et ouvert à tous sans inscription, ce qui en fait un lieu à part dans la vie intellectuelle française. Être nommé professeur au Collège de France est considéré comme une des plus hautes distinctions dans l'enseignement supérieur français.

    En théorie, la théorie et la pratique c'est pareil. En pratique c'est pas vrai.

    • [^] # Re: Collège de France

      Posté par  . Évalué à 6.

      L'enseignement y est gratuit et ouvert à tous sans inscription

      Avis perso : ça devrait être le cas de TOUS les cours en primaire, secondaire, partout.

      • [^] # Re: Collège de France

        Posté par  . Évalué à 6.

        Je suis plutôt d'accord pour l'enseignement supérieur (encore que dès qu'il y a des TD, l'aspect inscription est pratique).

        Par contre pour toute la partie de l'enseignement où le public est mineur, autant la gratuité et l'ouverture je suis complètement d'accord, autant l’absence d'inscription ça me semble tendu d'un point de vue logistique

        • [^] # Re: Collège de France

          Posté par  (Mastodon) . Évalué à 6.

          Idem, c'est sympa sur l'idée, mais faut penser à l'instit qui essaie un minimum de structurer son année.

          Dans le cadre du Collège de France, on parle d'un public adulte, érudit, qui peut piquer ici et là des cours sur un thème précis. Pas de gamins qui apprennent à lire écrire et compter.

          En théorie, la théorie et la pratique c'est pareil. En pratique c'est pas vrai.

          • [^] # Re: Collège de France

            Posté par  (site web personnel) . Évalué à 7.

            Puis le Collège de France ne propose pas de formation diplômante, à cause notamment de l'absence d'inscriptions et de suivi du cours.

            Donc ce principe est génial pour la culture générale. Pour ceux qui ont l'opportunité d'y assister. Mais si tu souhaites acquérir du savoir pour te reconvertir, cela peut être difficile à valoriser sur le marché du travail.

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.