Pourquoi ne pas simplement utiliser Lean ?

 (lawrencecpaulson.github.io)
1 points par GN⁺ 1 일 전 | 1 commentaires | Partager sur WhatsApp
  • L’histoire de la formalisation des mathématiques n’a pas commencé avec Lean, et différents systèmes de plusieurs lignées ont déjà accumulé les techniques essentielles et des résultats majeurs depuis près de 60 ans
  • Des outils comme AUTOMATH en 1968, la famille LCF, HOL, Rocq, ACL2 et Mizar ont permis de vastes formalisation, de l’analyse réelle jusqu’au théorème des nombres premiers, au théorème des quatre couleurs et à la conjecture de Kepler
  • Lean a rapidement accumulé des définitions de mathématiques modernes grâce à une grande bibliothèque et une communauté active, mais propositions as types et les types dépendants ne constituent pas l’unique voie pour les proof assistants
  • Isabelle met en avant une automatisation puissante, une grande lisibilité et l’évitement des types dépendants, tout en prolongeant la tradition LCF qui organise la vérification des preuves via la barrière d’abstraction du noyau, sans proof objects
  • Avec l’essor de l’IA, qui met en forme des preuves structurées et les traduit d’un système à l’autre, la pression consistant à considérer un seul outil comme référence absolue pourrait encore diminuer

Les premiers systèmes et les autres lignées

  • AUTOMATH

    • AUTOMATH contenait déjà en 1968 la plupart des éléments nécessaires à la formalisation des mathématiques
    • En 1977, Jutting a formalisé avec AUTOMATH Foundations of Analysis de Landau, en partant de la logique pure jusqu’à la construction des nombres complexes
    • Il utilisait des classes d’équivalence et l’ensemble des rationnels, et démontrait aussi formellement la complétude de Dedekind de la droite réelle
    • Cet exploit n’a pas été reproduit pendant 20 ans, et il a fallu attendre le milieu des années 1990 pour revoir une formalisation des réels avec HOL Light de John Harrison et Isabelle/HOL de Jacques Fleuriot
    • La notation était très peu pratique et il n’y avait aucune automatisation, ce qui rendait les preuves longues et difficiles à lire
    • Malgré cela, l’approche est jugée meilleure que Rocq pour manipuler les classes d’équivalence : contrairement au setoid hell rencontré par les utilisateurs de Rocq, Jutting a mené cette formalisation avec calme et méthode

  • Boyer et Moore

Les évolutions après LCF

  • Edinburgh LCF se concentrait sur la théorie des langages de programmation, mais l’idée d’utiliser un langage fonctionnel comme métalangage du proof assistant s’est largement diffusée
  • Des groupes à Cambridge, à l’INRIA, à Cornell et ailleurs ont utilisé ML pour créer des outils comme HOL, Coq (aujourd’hui Rocq) et Nuprl
  • Le groupe HOL s’est concentré sur la vérification matérielle, mais la vérification du matériel en virgule flottante a fini par exiger de l’analyse réelle
  • John Harrison a démontré dans la lignée HOL de véritables résultats mathématiques comme le théorème des nombres premiers via la formule intégrale de Cauchy
  • Avec l’objectif de vérifier le plus grand nombre possible parmi les 100 theorems, HOL Light figurait souvent tout en haut du classement
  • Jusqu’en 2014, ces systèmes de cette lignée avaient formalisé plusieurs théorèmes avancés
  • Ces théorèmes impliquaient en général des preuves longues et complexes, avec des projets de formalisation de très grande ampleur, jouant un rôle clé pour réduire les zones d’incertitude restées dans les démonstrations

L’essor de la communauté Lean

  • Des mathématiciens estimaient que les formalisation précédentes n’allaient pas jusqu’aux constructions raffinées des mathématiques contemporaines dominantes, comme les schémas de Grothendieck ou les espaces perfectoïdes
  • Tom Hales a choisi de construire ces définitions sous forme de bibliothèque, en privilégiant l’accumulation de définitions plutôt que les preuves, et a pour cela choisi Lean
  • Il a présenté cette orientation dans le programme Big Proof, où des idées voisines ont aussi été discutées
  • Kevin Buzzard, après cela, a décidé d’essayer Lean dans l’enseignement, ce qui a ensuite accéléré sa diffusion
  • Un tournant important de la communauté Lean est présenté comme l’abandon de l’obsession pour la preuve constructive qui a longtemps dominé Rocq
  • L’intuitionnisme est apparu après le paradoxe de Russell et impliquait aussi une certaine conception des nombres réels
  • La théorie des types de Martin-Löf est clairement un formalisme intuitionniste, mais il est indiqué qu’on ne peut pas réduire Rocq à cela de manière aussi simple
  • Malgré tout, dans les articles liés à Rocq, les preuves constructives revenaient sans cesse, même quand elles étaient hors sujet ou dénuées de sens, et cette tendance aurait freiné l’usage mathématique de Rocq au profit de Lean

Propositions as types et la différence LCF

  • Propositions as types désigne la dualité entre les symboles logiques ∀, ∃, →, ∧, ∨ et les constructeurs de types Π, Σ, →, ×, +
  • Ce cadre est élégant et théoriquement fécond, mais ce n’est pas la seule voie
  • Si l’on définit les proof assistants uniquement comme des logiciels qui vérifient les preuves selon le principe de propositions as types, alors la majeure partie de la recherche du dernier demi-siècle se retrouve exclue de la définition
  • Il ne resterait alors plus que Rocq, Lean et Agda
  • Même AUTOMATH n’est pas un exemple de propositions as types : bien qu’il comporte des éléments proches de Π et de →, la logique y est posée par axiomes, comme dans un manuel classique de logique
  • Il y a déjà 50 ans, de Bruijn estimait qu’il fallait séparer les types et les propositions
  • L’exemple typique est la division, qui doit prendre trois arguments, et où la valeur de (x/y) dépend d’une preuve de (y \ne 0), ce qui rend proof irrelevance nécessaire
  • L’idée selon laquelle l’approche LCF serait identique à propositions as types est elle aussi déclarée fausse
  • Rocq et Lean possèdent le sort Prop pour les propositions, dans lequel tous les objets de preuve d’une même proposition sont évalués comme la même valeur, ce qui fournit proof irrelevance
  • Cela ne fait toutefois pas disparaître les gigantesques objets de preuve, qui restent bien présents dans les systèmes réels
  • La découverte fondamentale de Robin Milner est qu’en LCF, les objets de preuve eux-mêmes ne sont pas nécessaires
  • Il suffit de placer le noyau de preuve dans un type de données abstrait de ML et de faire des règles d’inférence ses constructeurs pour vérifier dynamiquement les preuves
  • Grâce à la barrière d’abstraction de ML, il devient impossible de tricher
  • À l’ère de RAMmageddon, voir d’énormes termes occuper des dizaines de Mo alors qu’ils n’indiquent rien de plus paraît particulièrement irrationnel
  • Le texte critique aussi le fait que des recherches visent à rendre plus élégants de tels termes pourtant inutiles

Pourquoi choisir Isabelle

  • Si ses collègues utilisent Lean, que l’expertise de l’équipe est sur Lean et que les bibliothèques préalables nécessaires existent en Lean, il est naturellement logique de choisir Lean
  • Mais si le choix reste ouvert, il existe de bonnes raisons d’examiner Isabelle

  • Automatisation

    • Son atout serait l’automatisation la plus puissante, et même parmi les “hammer” courants, rien n’égalerait sledgehammer
    • Il est aussi précisé que l’algèbre informatique mériterait d’être traitée séparément

  • Lisibilité

    • Isabelle est présenté comme la meilleure option en matière de lisibilité, avec comme appui des exemples autour d’Isar

  • Évitement des types dépendants

    • L’absence de types dépendants permet d’éviter les universe levels et diverses étrangetés qui déconcertent les débutants
    • Il est aussi affirmé que l’usage des types dépendants n’est pas recommandé dans mathlib de Lean ni dans SSReflect et Mathematical Components de Rocq
    • La difficulté centrale des types dépendants est que, si on les implémente correctement, la vérification de types elle-même devient indécidable
    • Cela vient du fait que la décision d’égalité devient indécidable, point qui était initialement accepté comme allant de soi
    • À partir des années 1990, le consensus a évolué vers une réduction de l’égalité à la definitional/intensional equality afin de rendre la vérification de types décidable
    • En conséquence, (T(N+1)) et (T(1+N)) deviennent des types différents
    • Ces limitations ont des effets concrets sur les preuves, et le test de definitional equality reste lui-même coûteux en calcul

Des mathématiques modernes possibles sans types dépendants

  • L’auteur explique qu’en 2017, il était bien plus prudent sur ce qu’Isabelle pouvait réellement prendre en charge en mathématiques
  • À l’époque, il semblait facile de croire que des sujets comme les suivants exigeaient absolument des types dépendants
  • Mais les travaux liés à Alexandria ont beaucoup appris sur le sujet, et la conclusion essentielle est qu’il ne faut pas tout forcer dans les types

Orientation future et IA

  • Lean a bien fait beaucoup de choses et prend même en charge les blocs de preuve imbriqués, ce qui lui donne potentiellement un langage de preuve suffisamment lisible
  • Il faut maintenant que la communauté Lean utilise réellement ces possibilités, alors que les utilisateurs d’Isabelle le font déjà en grande partie
  • Plus que les objets de preuve vérifiables par machine, c’est la transparence d’un texte de preuve réellement lisible par un humain qui compte
  • L’essor de l’IA rend cette différence encore plus visible
  • Les preuves produites par l’IA sont souvent désordonnées, mais il est facile de les remettre en forme avec sledgehammer, et si leur structure est bonne, elles restent lisibles même avec trop de détails
  • Cela aide ensuite à suivre le fil du raisonnement et à les réduire à une forme plus simple
  • Des travaux récents montrent même des modèles de langage qui appellent directement sledgehammer
  • L’IA peut aussi faciliter la traduction de preuves structurées et lisibles d’un proof assistant à un autre
  • Dans ce cas, le poids même du choix d’un système pourrait diminuer

Complément sur l’oubli de Mizar

  • L’histoire de la formalisation des mathématiques ne peut pas être complète sans Mizar et son immense bibliothèque mathématique
  • Le langage Isar d’Isabelle a lui aussi été fortement influencé par Mizar
  • L’auteur corrige séparément cet oubli et annonce qu’il parlera de Mizar dans un prochain texte

À lire aussi

1 commentaires

 
GN⁺ 1 일 전
Commentaires sur Hacker News

  • La plupart des lecteurs de HN sont plus proches de programmeurs que de mathématiciens, donc il paraît plus pratique d’aborder Lean du point de vue de la programmation que de celui de la preuve mathématique
    Comme livre qui traite Lean sous l’angle de la programmation fonctionnelle, https://leanprover.github.io/functional_programming_in_lean/ est vraiment bien
    J’apprends aussi Lean, donc j’ai peut-être encore un regard un peu trop optimiste de débutant, mais je vise justement à écrire et prouver du code de programmeur ordinaire, comme de vrais algorithmes de compression/décompression à la manière de l’exemple récent de lean-zip
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • En lisant ce livre, j’ai bricolé moi-même un simplificateur d’algèbre informatique basique en Lean
      https://github.com/dharmatech/symbolism.lean
      C’est un portage de code C#, et la puissance expressive de Lean est étonnamment grande
    • Pour ce genre d’usage, Dafny ne serait-il pas aussi une option comparable ?
      J’en avais vu un peu parler il y a quelque temps, mais je ne suis plus ce domaine de près récemment
    • Je me souviens d’exemples, dans les années 1990, où l’on expérimentait la preuve de correction logicielle, et il me semble qu’au final il y avait plus d’erreurs dans les annotations de preuve que dans le logiciel lui-même
      Et je vois deux obstacles supplémentaires. D’abord, il est déjà difficile de savoir ce que le logiciel doit faire, et ce que l’utilisateur veut faire n’est pas forcément la même chose que ce pour quoi le client paie
      Ensuite, la qualité du travail de beaucoup de développeurs est si faible qu’il est difficile d’espérer qu’ils maîtrisent mieux un langage de vérité qu’un langage comme Java
      Cela dit, le second point pourrait disparaître si on les remplace par des systèmes d’IA capables d’y apporter l’attention nécessaire, et là la situation pourrait changer
    • Je me demande ce qu’il en est de la programmation non fonctionnelle
      À mes yeux, la programmation fonctionnelle est déjà, comme les mathématiques qu’elle a laissées de côté, quelque chose de largement peu pertinent pour la plupart des programmeurs

  • L’auteur semble assez mal comprendre Lean, ce qui est d’autant plus surprenant qu’il a l’air de bien connaître le domaine
    Il semble penser que Lean conserve les objets de preuve tels quels et qu’au bout du compte il vérifie un unique objet de preuve géant où toutes les définitions sont déroulées, mais c’est loin de la réalité
    Lean implémente en pratique exactement la même optimisation que l’auteur encense comme avantage de LCF. Pour prendre une image, c’est comme faire une preuve en effaçant le tableau au fur et à mesure
    En Lean4, si on écrit avec theorem plutôt qu’avec def, l’objet de preuve n’est plus réutilisé ensuite, et ce n’est pas une simple optimisation mais une propriété centrale du langage. Un theorem est opaque
    Même s’il reste un terme de preuve, ce n’est que pour que l’utilisateur puisse le voir en mode interactif, et le kernel ne peut même pas se soucier de ce qu’était cet objet de preuve

    • Cela relève plus d’une différence conceptuelle que d’une différence d’implémentation
      Dans LCF, preuve et terme sont distincts, et à mon avis c’est ainsi que cela devrait être. Ce type de confusion à la Curry-Howard est inutile, mais beaucoup pensent que c’est la seule façon de faire des mathématiques sur ordinateur
      Si on veut, on peut aussi stocker et exploiter des preuves dans LCF, et dans Lean on peut aussi les éliminer par optimisation si on le souhaite
    • En théorie des types dépendants, un objet de preuve n’est au fond qu’un terme qui remplit un certain type ; dans ce cas, je me demande si cela signifie que l’implémentation de Lean peut construire des preuves sans créer de tels termes
    • Ça me paraît juste
      L’approche par type abstrait économiserait peut-être un peu de mémoire, mais ce ne serait qu’un facteur constant, pas une amélioration asymptotique
      Les plaintes disant que Lean gaspille des dizaines de Mo auraient été importantes dans les années 1980-90, mais aujourd’hui cela ne me semble plus être un avantage si décisif

  • On entend souvent dire que Lean est bon pour la programmation fonctionnelle, mais quand on vient d’Agda cela donne plutôt l’impression d’un downgrade assez grossier
    On dit aussi beaucoup de bien des tactiques, mais d’après mon expérience les tactics de Coq étaient plus puissantes et plus agréables à utiliser
    C’est peut-être simplement un biais de première impression, mais jusqu’ici j’ai l’impression que la force de Lean ne tient pas au fait qu’il fasse une chose mieux que tout le monde, mais plutôt au fait qu’il est globalement correct et qu’il a une grande communauté
    Je comprends pourquoi c’est attractif, mais je trouve dommage qu’on y perde un peu en beauté et en puissance

    • En fin de compte, c’est aussi une histoire d’effets de réseau
      Cela dit, ces effets paraissent durables sur le moment, alors qu’en pratique ils le sont souvent moins qu’on ne le croit. Si c’était vraiment le seul facteur important, Perl devrait encore être un poids lourd aujourd’hui
      Dans le cas de Lean, le fait d’avoir constitué tôt une grande bibliothèque a été particulièrement important, un peu comme CPAN pour Perl
      Mais quand on regarde les lois d’échelle, la valeur d’une grande bibliothèque n’augmente probablement que comme le logarithme de sa taille pour la plupart des utilisateurs
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      Au début, cet écart semble impossible à rattraper, mais il arrive un moment où il n’est plus nécessaire d’égaler la taille, car la facilité d’usage devient plus importante
      En plus, le portage de bibliothèques mathématiques est un travail qui convient bien aux LLM. La source est vérifiée, la cible peut être vérifiée aussi, et le chemin de raisonnement est généralement transposable
      Dit autrement, les LLM abaissent aussi plus qu’on ne l’aurait cru la barrière à l’entrée pour travailler sur des plateformes minoritaires. Si je peux porter leur bibliothèque vers ma plateforme, il y a de fortes chances que je puisse aussi y porter mes preuves
    • Au contraire, cela ressemble plutôt au signe que la communauté a enfin mûri et commence à faire du vrai travail
      L’essentiel n’est pas d’avoir l’outil parfait, mais d’arriver à faire le travail avec un outil suffisamment bon
    • Agda est meilleur comme vérificateur de preuves, mais pas comme choix pratique pour produire du logiciel
      Lean semble avoir le potentiel de devenir un véritable successeur de Haskell, en tant que langage fonctionnel de développement logiciel
    • J’ai un peu utilisé Agda et davantage Lean, et pour écrire des programmes fonctionnels ordinaires plutôt que des preuves mathématiques, Lean était de très loin le plus simple
      La différence venait surtout du support outillage. La documentation d’Agda est faible, l’installation et la mise en route du système sont pénibles, et on a pratiquement l’impression qu’il faut utiliser Emacs
      À l’inverse, Lean a dans sa propre documentation jusqu’à la manière d’écrire un utilitaire cat, et donne globalement une expérience de tooling bien plus moderne
    • Je me demande ce qui est exactement meilleur en programmation fonctionnelle avec Agda
      En général, les éloges portent surtout sur le dependent pattern matching, et sur ce point Lean me paraît assez faible
      Mais si tu trouves aussi Agda plus agréable pour le FP en général, j’aimerais bien savoir en quoi précisément

  • Isabelle/HOL a un langage correct, mais son outillage présente des défauts profonds qui dépassent simplement une approche centrée desktop
    Le langage n’est pas si différent de Lean, sans être forcément meilleur, et je partage certaines critiques sur les types dépendants
    Au final, les deux langages ont fait des compromis différents, et ces choix semblent en avoir fait des outils assez efficaces chacun dans leur domaine. Le domaine de la preuve est lui-même vaste, donc chaque paradigme a ses forces et ses faiblesses, et Lean s’est simplement spécialisé sur une autre partie du problème
    Sledgehammer est bien, mais l’arrivée de quelque chose de similaire dans Lean semble n’être qu’une question de temps
    Cela peut être utile en phase d’exploration, mais c’est gourmand en ressources, et même si cela raccourcit les preuves, dans du code publié je préfère voir toutes les étapes de la preuve explicitement plutôt qu’un by sledgehammer à moitié magique
    En revanche, développer Isabelle lui-même est bien plus pénible que Lean, et c’est particulièrement vrai dans les échanges avec les développeurs
    Sur la mailing list, l’attitude du genre il n’y a pas de bug, seulement des comportements inattendus m’a paru puérile et peu professionnelle
    Et se moquer de l’usage RAM de systèmes similaires à Lean est assez cocasse quand on voit la gloutonnerie mémoire du côté d’Isabelle

    • Le problème ici, c’est que produire des certificats UNSAT sous une forme vérifiable rapidement n’a rien de trivial
      En pratique, c’est presque aussi difficile que d’utiliser une preuve formelle en tant que telle
    • La dernière fois que j’ai vérifié, Isabelle/HOL utilisait comme interface un mode Emacs personnalisé
      Il est possible que je confonde avec un autre HOL
    • Je ne sais pas exactement ce qu’est Sledgehammer, mais à la description cela ressemble presque au même type d’outil que grind dans Mathlib
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Ce qui est intéressant avec Lean, c’est que Lean est un langage, alors que ce dont les gens parlent le plus est en réalité une bibliothèque, Mathlib
    Les créateurs de Mathlib semblent assez pragmatiques, et c’est sans doute pour cela qu’ils intègrent la logique classique dans les types Lean tout en n’utilisant qu’une partie de la logique intuitionniste

    • L’exemple donné pour expliquer le tiers exclu est faux
      Dire que « quelque chose ne peut pas être à la fois vrai et faux » ne correspond pas au tiers exclu mais au principe de non-contradiction
      Le tiers exclu signifie que p est vrai ou que not p est vrai
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • Côté informatique, ils sont désormais en train de construire leur propre CSLib
      https://www.cslib.io https://www.github.com/leanprover/cslib
      La logique intuitionniste a fondamentalement un intérêt quand il s’agit de transformer des raisonnements mathématiques en constructions calculables, donc je trouve intéressant de voir comment cette question sera traitée
      En réalité, dès qu’on écrit des algorithmes en Lean, on entre déjà d’une certaine manière dans des contraintes constructives, et ce niveau de logique est peut-être suffisant pour cet objectif
    • Cela me fait penser à la blague sur les cinq étapes de l’acceptation des mathématiques constructives
      déni, colère, négociation, dépression, acceptation
      Les conférences et articles d’Andrej Bauer sur le sujet valent aussi le détour
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • Ici, il faudrait parler non de intuitive logic, mais de intuitionistic logic
    • Malgré toutes ces contraintes et ces blocages, je me demande quand et pourquoi on finit par préférer la logique intuitionniste

  • Je pense qu’il nous faut plus d’articles de ce genre
    Même face au conformisme qui pousse tout le monde à dire utilisez simplement X, il y a toujours au moins de bonnes raisons d’examiner les alternatives
    Et même si l’on finit par écarter ces alternatives pour choisir la solution dominante, il vaut mieux le faire en connaissance du terrain

    • Je ne suis pas totalement d’accord
      On fabrique déjà trop de frameworks et d’alternatives, et probablement encore plus parce que c’est amusant
      Au lieu d’améliorer les outils existants ou simplement d’avancer sur le travail réel, on finit souvent par multiplier sans fin langages, bibliothèques et build tools
      À mon avis, on se porterait mieux s’il y avait deux fois moins de langages, de bibliothèques et d’outils de build qu’aujourd’hui
    • Au final, ça dépend du contexte
      Plus on s’éloigne du mainstream, plus la documentation diminue, plus il y a de bugs dans les coins moins explorés, et moins il y a de gens pour aider
      Quand il y a plus d’une vingtaine d’options, en moyenne il vaut mieux choisir l’option standard et passer à autre chose. L’attention est une ressource finie ; si on rédige un rapport d’étude pour chaque dépendance, on ne résout plus le problème principal
      Il y a toutefois deux exceptions : quand l’outil standard ne correspond pas vraiment à mon cas d’usage, ou quand l’outil standard recoupe fortement le problème central que j’essaie de résoudre

  • Ce type de discussion me rappelle les articles qui pointent les limites de Python en calcul scientifique
    Une fois qu’une communauté atteint une masse critique autour d’un outil suffisamment correct, cela finit par écraser la plupart des autres facteurs
    L’élan s’enclenche, les tutoriels, articles explicatifs et meilleures documentations s’accumulent, et l’on atteint en pratique une sorte de vitesse de libération
    Lean semble être exactement dans cette position aujourd’hui, avec même des soutiens de poids comme Terrance Tao
    Donc dire que « le langage X est meilleur » n’est pas complètement faux, mais cela fait facilement passer à côté de la vraie question
    La vraie question, c’est de savoir s’il est réellement meilleur que l’outil que tout le monde connaît, peut utiliser immédiatement, et dans lequel davantage de temps est investi pour l’améliorer
    Au fond, cela ressemble à une situation de worse is better, ou à l’idée qu’être bon et populaire suffit largement

    • Je trouve très juste l’idée que les LLM vont rendre assez efficace la traduction entre systèmes formels différents
      Surtout dans ce domaine, où le résultat de la traduction peut en grande partie être vérifié automatiquement, le choix lui-même n’est peut-être pas si crucial
    • Mais à l’ère de l’IA, l’importance de la masse critique est bien moindre
      L’IA peut écrire du code par elle-même même sans immense bibliothèque communautaire, et elle lit directement la documentation et les spécifications sans avoir besoin d’un million de tutoriels sur Internet
      Il n’est pas non plus nécessaire d’éviter les langages sans marché de l’emploi. L’IA ne construit pas une carrière, elle fait simplement le travail qu’on lui donne à l’instant
      Donc même des petits langages et DSL qui n’auraient autrefois eu aucune chance peuvent désormais être adoptés plus facilement
      Je pense aussi que la monoculture linguistique qui a longtemps dominé en programmation pourrait prendre fin avec l’IA

  • Dire que « presque tout ce qui est formalisé aujourd’hui dans n’importe quel système pourrait aussi l’avoir été dans AUTOMATH » revient un peu à dire qu’aujourd’hui tout ce qu’on code dans un langage moderne aurait aussi pu être codé en assembleur il y a 50 ans
    C’est techniquement vrai, mais économiquement cela n’a rien à voir

    • Les langages assembleur sont généralement Turing-complets, mais je ne vois pas très bien quel serait l’équivalent exact de cette comparaison du côté des moteurs de preuve

  • Il y a une quinzaine d’années, j’avais essayé de toucher à Coq/Rocq et à quelques autres outils, et j’avais eu beaucoup de mal à comprendre le logiciel lui-même plus encore que les concepts
    Ce qui est étrange avec les assistants de preuve / démonstrateurs de théorèmes interactifs, c’est que leur nature interactive fait qu’ils deviennent une sorte de combinaison entre langage et IDE, et qu’en pratique les deux sont fortement liés
    Il est donc difficile de parler du langage isolément ; il faut aussi regarder dans quel environnement on l’utilise
    Je ne suis pas non plus un fan absolu de VS Code, mais il est clair qu’un IDE extensible utilisé par énormément de gens, peaufiné à grand renfort d’investissements, est très en avance sur les environnements proposés par les alternatives
    D’excellents parcours d’introduction comme Natural Numbers Game semblent aussi rendus possibles par la capacité de VS Code à être bidouillé et par tout son écosystème
    En apprenant Lean, ce qui m’inquiète en revanche, c’est que l’extensibilité syntaxique soit une arme à double tranchant
    Une fois le langage appris, on a envie de lire du code écrit dans ce langage ; mais si chaque projet commence à fabriquer toute une collection de DSL maison, cela peut vite devenir ingérable
    Au final, tout dépendra de la retenue de la communauté et de l’écosystème, donc je regarde cela avec à la fois de l’espoir et de l’inquiétude

  • Lean n’est ni l’assistant de preuve le plus aimé des mathématiciens, ni l’outil le plus adapté à la vérification formelle de logiciels
    En revanche, il se débrouille correctement dans les deux cas, et surtout il a réussi à capter l’élan le plus difficile à obtenir : le momentum
    Et à l’ère de l’IA, comme la quantité de code écrit par des humains disponible publiquement influe directement sur la capacité des agents à produire correctement du nouveau code, cet élan devient encore plus fort