Depuis l'an dernier, Xavier Leroy est le nouveau titulaire de la chaire « sciences du logiciel » au Collège de France. J'en avais fait un journal pour présenter le thème de sa première année de cours où il abordait la correspondance entre programmes et démonstrations mathématiques, connue sous le nom de correspondance de Curry-Howard.

Cette année, il a décidé d'aborder la formalisation de la sémantique des langages de programmation avec l'aide de la machine (en utilisant l'assistant de (…)

À 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 (…)

Au détour de mes pérégrinations sur la toile, je suis tombé sur un fil au contenu amusant et étonnant sur le stack exchange Unix. Mais que fait la commande man après minuit ? Se transforme-t-elle en Gremlins si on lui donne à manger ? Non, elle se met à chanter ! mais à une heure bien précise. :-)

Cet easter egg est resté confidentiel pendant 6 ans. Il fut introduit par ce commit et trouve son origine dans une blague faite sur (…)

Certains d'entre vous ont peut-être vu passer l'information : les derniers processeurs Intel des familles Skylake et Kaby Lake sont victimes d'un bug lorsque l'hyperthreading est activé. On trouve par exemple un article sur Ars Technica, et Debian propose des instructions détaillées pour corriger le problème en mettant à jour le firmware du CPU.

Néanmoins, dans ce journal, je vais revenir sur les événements qui ont mené à la découverte du problème. Xavier Leroy le décrit en détail (…)

Le 17 avril, le projet Debian a appris l'arrestation de Dmitry Bogatov (en) par les autorités russes.

Dmitry Bogatov est un enseignant en mathématiques, et un contributeur Debian actif. En tant que mainteneur Debian, par exemple, il travaillait dans le groupe Haskell et maintenait actuellement de nombreux paquets d'outils systèmes et en ligne de commande.

Pour le moment, les raisons de son arrestation et ce qui lui est reproché ne sont pas connues. Le projet a tout de même pris (…)

En cette période électoral, dans la lignée de certains journaux polémiques de ces derniers jours, je me devais de faire un journal pour relater le résultat d'une élection tombé hier. Non, il ne s'agit pas du résultat du référendum s'étant déroulé en Turquie ! On est sur LinuxFr.org, on y parle de logiciels libres et de ce qui gravite autour du libre en général. Je parlerais donc de l'élection du nouveau leader d'une des distributions majeures (et celle que j'utilise) (…)

Hier, jeudi 24 novembre 2016, Xavier Leroy a reçu le prix Milner à Londres à la Royal Society. Le prix Milner est le plus grand prix européen en informatique; il est décerné conjointement par la Royal Society, l'Académie des Sciences et l'académie allemande Leopoldina. Il est décerné en l'honneur de l'informaticien britannique Robin Milner qui fut lauréat du Prix Turing en 1992.

Le prix revient cette année à Xavier Leroy pour ses travaux tant théoriques que pratiques sur la fiabilité (…)

Dans la lignée du journal EDSL et F-algèbres, ce journal présente une méthode pour plonger un langage dans un autre (ici OCaml) qui généralise la précédente et centrée autour de la notion d'interprétation. Contrairement aux méthodes plus courantes pour résoudre cette question, la méthode tagless-final permet également de résoudre le problème de l'extensibilité : étendre un type de donnés, ajouter des opérations dessus, sans avoir à réécrire du code déjà compilé et cela avec la sécurité du (…)