Sciences du logiciel - Xavier Leroy Leçon inaugurale - Xavier Leroy : Le logiciel, entre l'esprit et la matière
4 snips
Nov 15, 2018 
Xavier Leroy, informaticien renommé et architecte du langage OCaml, partage sa passion pour les langages de programmation et la vérification formelle. Il explore l'évolution des logiciels, des origines mécaniques à l'impact de l'IA sur la programmation. Leroy évoque la complexité et les défis de la vérification formelle, tout en discutant de la correspondance entre types et preuves. Il met en lumière des projets emblématiques comme CompCert, soulignant la nécessité d'une spécification précise pour garantir la sûreté des logiciels.
AI Snips
Chapters
Books
Transcript
Episode notes
Programmabilité Comme Révolution Technique
- Xavier Leroy retrace l'histoire du logiciel depuis les métiers à tisser jusqu'à l'ordinateur programmable universel.
- Il montre que la programmabilité a transformé le matériel en tabula rasa offrant une flexibilité inédite.
Naissance De La Calculabilité Moderne
- Church et Turing formalise(nt) l'idée d'algorithme et établissent l'équivalence de modèles de calcul.
- Cette universalité définit la notion moderne de calculabilité et fonde l'informatique théorique.
Efficacité Complète La Calculabilité
- La calculabilité seule est insuffisante ; il faut mesurer l'efficacité et la programmabilité.
- L'algorithmique et la programmation apportent les notions de complexité et d'efficacité nécessaires.
