Pourquoi je n’utilise pas les types dépendants

• La théorie des types dépendants inclut des objets de preuve, mais l’auteur la considère comme une structure inutile et inefficace
• Après avoir étudié directement d’anciens systèmes fondés sur les types dépendants comme AUTOMATH et le système formel de Martin-Löf, Isabelle a évolué vers un framework logique générique
• Basé sur la théorie des types simples (logique d’ordre supérieur), Isabelle/HOL se distingue par son automatisation, ses bibliothèques à grande échelle et sa lisibilité
• Le projet ALEXANDRIA a démontré qu’il est possible de formaliser des théorèmes mathématiques avancés avec la seule logique d’ordre supérieur
• Malgré la maturité de systèmes à types dépendants comme Lean, l’auteur continue de préférer la praticité de l’approche en logique d’ordre supérieur en raison de problèmes de performances et de complexité

---

Types dépendants et objets de preuve

• Dans la théorie des types dépendants, les objets de preuve (proof objects) sont indispensables, mais l’auteur les considère comme un gaspillage d’espace
  • Dans l’architecture LCF, seules des étapes de preuve valides peuvent être exécutées grâce à une vérification de types au niveau du langage d’implémentation, et non à l’intérieur de la logique
  • L’intuition de Robin Milner a introduit le concept de proof kernel, qui est devenu la base d’Isabelle
• À la question « pourquoi ne pas avoir utilisé les types dépendants ? », l’auteur répond : « je les ai utilisés pendant longtemps »

Expérience avec AUTOMATH

• En 1977, à Caltech, il a assisté au cours de N. G. de Bruijn sur AUTOMATH, sans pouvoir utiliser directement le système
  • Le système de l’université d’Eindhoven n’était alors pas connecté à l’ARPAnet, et il fallait un ordinateur basé sur ALGOL 60
• AUTOMATH est un système à types dépendants, mais il n’implémente pas la correspondance de Curry–Howard
  • L’utilisateur devait ajouter comme axiomes les symboles et règles d’inférence de la logique souhaitée
  • de Bruijn comparait cela à « un grand restaurant qui sert tous les plats »
• Isabelle a repris cette idée en visant la généralité comme framework logique
  • Mais de Bruijn détestait la théorie des ensembles et voyait les mathématiques comme fondamentalement fondées sur les types
• L’auteur a interrogé AUTOMATH sur la vérification de la correction, et de Bruijn lui a envoyé un traité de théorie du langage (300 pages), sans le convaincre

Théorie des types de Martin-Löf

• À Chalmers, à Göteborg, il a étudié la théorie des types de Martin-Löf et a été séduit par la possibilité de synthèse de programmes
  • Il la jugeait clairement « juste » en ce qu’elle implémentait directement les principes de la logique intuitionniste de Heyting
• Il a poursuivi ces recherches pendant des années et a implémenté les premières versions d’Isabelle dans la théorie de Martin-Löf
  • Elle est toujours distribuée aujourd’hui sous la forme de Isabelle/CTT
• Mais l’atmosphère dogmatique centrée sur Per Martin-Löf et le passage imposé à l’égalité intentionnelle (intensional equality) ont fait échouer ces travaux
• Les systèmes apparus ensuite, comme le Calculus of Constructions (CoC), Rocq et Lean, ont laissé subsister les mêmes interrogations
  • Le CoC a accumulé pendant des décennies diverses variantes et des axiomes optionnels

Choix de recherche et orientation d’Isabelle

• Les chercheurs doivent choisir entre développer un nouveau système formel et étendre ou exploiter un système existant
  • Isabelle a été conçue comme un framework généralisé capable d’accueillir différentes logiques
• En 1985, Mike Gordon a effectué de la vérification matérielle avec la théorie des types simples de Church
  • Plus tard, John Harrison a conçu un encodage de la dimension des vecteurs
• Isabelle/HOL ajoute à la théorie de Church des classes de types axiomatiques et le système de modules locale
• La communauté Lean a accompli une vaste formalisation des mathématiques (mathlib) sur une base CoC

Projet ALEXANDRIA et test des limites de la logique d’ordre supérieur

• Le projet ALEXANDRIA, financé par l’ERC, met en avant l’automatisation, les bibliothèques et la lisibilité d’Isabelle
• Au départ, on pensait que la logique d’ordre supérieur atteindrait ses limites, mais en pratique, des mathématiques avancées comme les schémas de Grothendieck ont été formalisées avec succès
  • Paulo Emílio de Vilhena et Martin Baillon ont démontré que tout corps admet une extension algébriquement close
• Le projet s’est étendu jusqu’à des résultats avancés comme le théorème de Balog–Szemerédi–Gowers
  • L’affirmation selon laquelle « il est impossible de formaliser les mathématiques sans types dépendants » a disparu, et il ne reste plus que l’argument selon lequel « les types dépendants sont plus élégants »

Position actuelle sur Lean et les types dépendants

• L’auteur envie la taille de la communauté de Lean et l’outil Blueprint, mais les problèmes de performances et la complexité demeurent
  • Les conflits avec l’égalité intentionnelle et la difficulté à savoir quand utiliser les types dépendants sont régulièrement signalés
• L’auteur compare les types dépendants au Full Self-Driving de Tesla, en pointant des attentes excessives et des désagréments bien réels

Annexe : limites théoriques de la logique d’ordre supérieur

• Certains affirment que la logique d’ordre supérieur est faible du point de vue de la théorie de la démonstration, mais cela signifie seulement qu’elle est plus faible que la théorie des ensembles ZF
• D’après les résultats d’ALEXANDRIA, la logique d’ordre supérieur peut malgré tout traiter des structures mathématiques complexes comme les schémas de Grothendieck
  • Seules deux preuves ont nécessité l’ajout des axiomes ZF, et il s’agissait de théorèmes mentionnant directement des objets ZF

Notes

• L’intuitionnisme est une philosophie qui considère le langage comme un simple moyen d’enregistrement, et diffère des mathématiques constructives (constructive mathematics) d’aujourd’hui

[GN⁺]

Avis Hacker News

• Les types dépendants sont très utiles dans certaines situations
  Par exemple, ce serait bien si Python pouvait exprimer et vérifier par le typage une « matrice float32 de taille 10×5 »
  Mais des concepts comme la correspondance de Curry–Howard, qui identifient preuve et type, sont déroutants du point de vue humain
  Une erreur de type ressemble à une simple faute qu’on peut corriger, tandis qu’une erreur de preuve est un problème bien plus complexe qui demande de la réflexion
  C’est pourquoi, à mon avis, la vraie force de Lean n’est pas son système de types, mais sa communauté et la structure open source de mathlib
  Alors que l’AFP d’Isabelle fonctionne comme une revue académique, Lean a une collaboration très active fondée sur les pull requests
  Je développe actuellement un nouveau démonstrateur de théorèmes, Acorn(acornprover.org), avec l’idée de combiner les avantages de Lean et d’Isabelle
  La puissance d’expression simple des types dépendants de Lean est appréciable, mais si on en abuse, le débogage devient difficile

  • En C++ ou en Rust, on peut aussi exprimer ce genre de types pour des tableaux de taille constante
    En revanche, on ne peut pas garantir à la compilation la plage d’un indice qui n’est connue qu’à l’exécution
    Un vrai langage à types dépendants peut prévenir les erreurs d’exécution au niveau du type
  • Avec les const generics de Rust ou les non-type template parameters de C++, c’est déjà largement faisable
    En pratique, même dans les langages à types dépendants, on utilise rarement les types dépendants pour empêcher les erreurs d’exécution,
    ils servent surtout à exprimer des invariants de structures de données ou à vérifier un programme après sa définition
    Références associées : division-by-zero in type theory FAQ, présentation de Xavier Leroy
  • On peut aussi imiter un peu les types dépendants en TypeScript
    Par exemple, comme à la ligne 38 de ce code, on peut représenter la taille d’une matrice par le type
    J’ai aussi implémenté un type de vecteur et le type résultat d’une multiplication de matrices
    Cela dit, ce n’est pour l’instant qu’une expérimentation personnelle, et ce n’est peut-être pas adapté à des projets de données à grande échelle
  • La formule « la preuve est identique au type » est intéressante
    Cela renvoie au concept de Propositions as Types
    Je me demande comment les types dépendants fonctionnent à l’exécution, et s’il faut à la fois une vérification de types à la compilation et à l’exécution
    Je me demande aussi si l’implémentation ne crée pas une complexité accrue avec beaucoup d’indirections
  • Dire qu’on veut exprimer en Python un type de matrice 10×5, cela ne revient-il pas simplement à dire qu’il suffit de le définir directement comme une classe ?

• L’argument du Dr Paulson n’est pas que les types dépendants sont mauvais, mais qu’ils ne sont pas indispensables
  J’aurais aimé voir davantage de discussion sur les problèmes de performance de Lean ou sur l’égalité intentionnelle
  Comme avec le HEq d’Isabelle(lien), les cas qui ne relèvent pas de l’égalité définitionnelle posent problème
  C’est pourquoi je pense qu’il vaut mieux utiliser les types dépendants aussi peu que possible
  Même un système sans typage statique comme ACL2 permet des vérifications suffisantes
  Au final, ce qui compte, c’est l’équilibre entre praticité et vérifiabilité

  • Du point de vue de la vérification logicielle, Isabelle (non dépendant) est déjà largement assez puissant
    Lean ou Agda sont encore moins utilisés pour des vérifications à l’échelle industrielle
    Il est intéressant de comparer Concrete Semantics(lien) et Logical Verification 2025(lien)
    En pratique, les refinement types peuvent être plus utiles
    Exemples : Rust Creusot, Dafny, et l’exemple de preuve de leftpad pour LiquidHaskell
  • En mathématiques, les preuves ne servent pas de programmes, donc les types dépendants y fonctionnent bien
    Mais dans la vérification de programmes, il faut des lemmes auxiliaires complexes comme « ces deux preuves sont identiques », et cela est souvent impossible à prouver
  • Je me demande pourquoi il faudrait utiliser les types dépendants aussi peu que possible
  • Affirmer que ce n’est « pas nécessaire » ressemble à une esquive
    La vraie question est de savoir à quel point la fonctionnalité est utile, pas si son existence est nécessaire ou non
    Au fond, le choix d’un outil relève surtout des préférences du développeur et de l’efficacité

• Il est intéressant de voir qu’une grande partie des débats en logique moderne finit par relever de préférences esthétiques
  Si les avantages concrets étaient écrasants, il n’y aurait probablement pas de débat
  À ce propos, l’article de 1999 de Paulson et Lamport, « Typing in Specification Languages », vaut la lecture
  Depuis, un formalisme informel à la TLA+ de Lamport a aussi émergé

  • Pour moi, ce n’est pas simplement une question d’esthétique, mais de compromis
    On gagne les garanties à la compilation, mais on paie en complexité et en temps de build
    La vraie question est donc : « est-ce que cet échange en vaut la peine ? »

• Le problème de HOL (théorie des types simples) n’est pas la dépendance, mais son manque de force logique
  C’est l’équivalent d’une version restreinte de la théorie des ensembles de Zermelo, donc trop faible pour formaliser entièrement les mathématiques modernes
  Il est particulièrement difficile d’y traiter les problèmes de taille dans des domaines comme la théorie des catégories

  • Il existe un cas de formalisation de schémas de Grothendieck à l’aide de la fonctionnalité locales d’Isabelle
    Je serais curieux de savoir à quel point cela diffère du style des mathématiciens en pratique
  • Pour renforcer la puissance logique, on peut aussi ajouter des axiomes
    Par exemple, l’ajout d’un « cardinal inaccessible » rapproche le système de la notion d’« universe » en théorie des types

• J’ai étudié les méthodes formelles et je trouvais les types dépendants élégants, mais en pratique leur usage a toujours été un combat difficile
  Quand j’utilisais F#, j’ai essayé d’introduire F*, mais mes collègues trouvaient la courbe d’apprentissage mathématique trop lourde
  J’en suis finalement arrivé à la conclusion cynique que les ingénieurs apprennent mal les outils qui embarquent beaucoup de mathématiques

  • F* est davantage orienté vérification logicielle que mathématiques, donc son positionnement diffère de Lean
    Il permet un usage léger des types dépendants en s’appuyant sur la résolution de contraintes par SMT
    Mais cela ne répond pas à la question philosophique : « est-ce vraiment la bonne approche ? »
    Le monde de la preuve mathématique et celui de la vérification logicielle sont assez différents
  • Ce n’est pas que les gens refusent d’apprendre de nouvelles choses, c’est simplement qu’ils jugent le rapport coût/bénéfice insuffisant
    Au final, le temps est limité

• Dans notre entreprise Phosphor, nous expérimentons la combinaison des types dépendants avec des requêtes de base de données / de graphe
  Cela nous a permis de compenser les limites de RDF et de construire un système de requêtes fondé sur la logique
  En pratique, nous utilisons TypeDB(typedb.com), plus rapide que MongoDB et utile pour modéliser des données complexes
  C’est aussi proche de la notion d’ontologie chez Palantir

  • Je serais curieux d’avoir une explication plus concrète de la formule « construire un moteur de croissance non dilutif »
  • Je serais curieux de connaître les raisons du choix de TypeDB ainsi que les chiffres de performance obtenus en pratique

• Au fond, le secret des types dépendants est peut-être de savoir quand ne pas les utiliser
  Plutôt que de critiquer Lean ou Rocq, on pourrait peut-être, selon le contexte, adopter une approche plus proche du style Isabelle

• Le projet de formalisation Alexandria(lien) de l’équipe de Paulson est impressionnant
  En particulier, les travaux sur la formalisation d’algorithmes de calcul quantique(lien vers l’article) sont intéressants

• Autrefois, je croyais que les types dépendants représentaient l’avenir, mais dans les projets réels, la baisse de productivité était trop importante
  Aujourd’hui, je préfère des solutions claires et faciles à maintenir
  Si l’équipe peut comprendre l’outil et l’étendre, alors c’est probablement un bon outil

• Je préfère les systèmes de types qui se situent à la frontière des types dépendants plutôt que les types dépendants complets
  Par exemple, Purescript fournit nativement des row types plus puissants que ceux de Haskell,
  et prend aussi en charge les listes, chaînes et expressions régulières au niveau du type
  On peut s’en servir sous forme de programmation logique basée sur les typeclasses