Conférence proposée par : Guillaume Andrieu Catégorie : Langages Dans le vieux débat typage statique/typage dynamique, le typage statique semble gagner du terrain. Le typage statique s'est introduit dans le monde JS avec Typescript, et même dans Python avec ses "type hints" puis mypy. Mais les langages à typage statique eux-mêmes lorgnent vers plus de flexibilité, et tous jalousent en secret les capacités d'expression des langages à types dépendants. Même Haskell se voit doter de plusieurs initiatives pour y intégrer des types "liquides" ou carrément des types dépendants. Le typage dépendant est d'une simplicité conceptuelle radicale: là où de nombreux langages font une séparation nette entre valeurs et types (que des ~apprenti-sorciers~ développeurs astucieux s'évertuent souvent à contourner), les langages à types dépendants permettent aux types d'être des valeurs "comme les autres": des fonctions peuvent renvoyer des types, ou en prendre en arguments, et les types peuvent être paramétrés (ou "indexés", dans le jargon) par des valeurs. Alors certes, peu de langages ont ces particularités. Pourtant, apprendre à considérer les programmes comme des preuves a des bénéfices mêmes quand on ne dispose pas de ce type de typage dans son activité quotidienne. Lors de cette présentation, on découvrira les types dépendants à travers deux exemples simples, dans le langage Idris2. Le but est de réfléchir ensemble sur la notion de preuve en explorant les possibilités qu'offrent ce typage, notamment la possibilité d'écrire des preuves formelles. On appliquera notamment cette technique à l'optimisation d'une fonction, en prouvant formellement que notre optimisation n'a pas d'impact sur le comportement de la fonction. Nous en profiterons pour aborder la manière dont on peut s'inspirer de ces techniques dans d'autres langages. #DevFest #DevFestToulouse #GDG #GDGToulouse #Toulouse