Lean est dominant dans le domaine de la formalisation des maths, mais Agda avance pas mal aussi, et largement dans une autre direction puisque la plupart des gens qui font de la théorie homotopique des types (dans l'une de ses variantes, p.ex. la théorie cubique des types) le font en Agda (certains le font en Rocq aussi, mais Lean ne le permet pas du tout). Et j'ai l'impression que Rocq reste le plus utilisé pour la vérification de programmes, mais c'est peut-être mon biais d'observation qui fait ça (parce que je suis plus au contact de la recherche qui se fait en France, et Rocq est développé par l'Inria et beaucoup utilisé dans les labos français) ; en tous cas c'est sûr que CompCert et Iris, des outils assez connus, sont construits sur Rocq.
Quoi qu'il en soit, je pense qu'il ne faut pas le voir comme un concours : c'est une bonne chose qu'il y a plusieurs outils en parallèle, parce que ça leur fait explorer des pistes différentes, ça évite le lock-in exclusif à un outil qui empêche l'innovation ensuite, etc.
Quelques différences entre Rocq et Lean :
Lean a une grosse particularité dans sa théorie des types, qui s'appelle la « proof irrelevance définitionnelle », et qui peut être très pratique mais a aussi pour conséquence de casser plein de bonnes propriétés théoriques de la théorie des types. Notamment, le type checking de Lean est une approximation d'un problème indécidable, et contrairement à presque toutes les théories de types, il existe en fait des programmes qui ne terminent pas (des termes non fortement normalisables). Rocq a fini par introduire cette particularité sous une forme plus faible qui n'a pas ces conséquences désagréables, mais pour garder la compatibilité avec l'existant, ils l'ont fait avec un autre univers de propositions, du coup on a deux univers, SProp et Prop, qui coexistent, et SProp n'est pas très agréable en pratique parce que toutes les librairies existantes sont écrites avec Prop.
Globalement, il y a plus de vieilleries dans Rocq, c'est un peu normal vu son âge. Il y a plein de fonctionnalités qui font des choses similaires mais pas tout à fait identiques, souvent pour des raisons de compatibilité. (Ltac vs Ltac2 vs Mtac, tactiques standard vs SSreflect, inductifs simples vs records, classes de type vs instances canoniques, #[refine] vs Program, etc.) De plus la bibliothèque standard de Lean est vraiment beaucoup mieux faite. C'est subjectif mais je pense que la plupart des gens seront d'accord pour dire que Lean est mieux ingéniéré et a tiré des leçons de certains aspects moins bien faits de Rocq.
Comme il s'adresse largement à des matheux qui n'y connaissent rien à la logique intuitionniste, Lean n'a pas peur d'utiliser le tiers exclu, et aussi d'autres axiomes comme l'extensionnalité fonctionnelle, l'extensionnalité propositionnelle, les types quotients et l'axiome du choix. Ça n'empêche pas de raisonner sans ces axiomes en Lean, mais c'est lourdingue parce que toutes les tactiques standard les introduisent même quand elles n'en auraient pas besoin.
Rocq, en plus de permettre de faire de la théorie homotopique des types, a des options « expertes » et parfois expérimentales qui permettent de jouer avec les détails de la théorie des types, que n'a pas Lean.
[^] # Re: Lean vs Rock
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 4.
Lean est dominant dans le domaine de la formalisation des maths, mais Agda avance pas mal aussi, et largement dans une autre direction puisque la plupart des gens qui font de la théorie homotopique des types (dans l'une de ses variantes, p.ex. la théorie cubique des types) le font en Agda (certains le font en Rocq aussi, mais Lean ne le permet pas du tout). Et j'ai l'impression que Rocq reste le plus utilisé pour la vérification de programmes, mais c'est peut-être mon biais d'observation qui fait ça (parce que je suis plus au contact de la recherche qui se fait en France, et Rocq est développé par l'Inria et beaucoup utilisé dans les labos français) ; en tous cas c'est sûr que CompCert et Iris, des outils assez connus, sont construits sur Rocq.
Quoi qu'il en soit, je pense qu'il ne faut pas le voir comme un concours : c'est une bonne chose qu'il y a plusieurs outils en parallèle, parce que ça leur fait explorer des pistes différentes, ça évite le lock-in exclusif à un outil qui empêche l'innovation ensuite, etc.
Quelques différences entre Rocq et Lean :
Lean a une grosse particularité dans sa théorie des types, qui s'appelle la « proof irrelevance définitionnelle », et qui peut être très pratique mais a aussi pour conséquence de casser plein de bonnes propriétés théoriques de la théorie des types. Notamment, le type checking de Lean est une approximation d'un problème indécidable, et contrairement à presque toutes les théories de types, il existe en fait des programmes qui ne terminent pas (des termes non fortement normalisables). Rocq a fini par introduire cette particularité sous une forme plus faible qui n'a pas ces conséquences désagréables, mais pour garder la compatibilité avec l'existant, ils l'ont fait avec un autre univers de propositions, du coup on a deux univers,
SPropetProp, qui coexistent, etSPropn'est pas très agréable en pratique parce que toutes les librairies existantes sont écrites avecProp.Globalement, il y a plus de vieilleries dans Rocq, c'est un peu normal vu son âge. Il y a plein de fonctionnalités qui font des choses similaires mais pas tout à fait identiques, souvent pour des raisons de compatibilité. (Ltac vs Ltac2 vs Mtac, tactiques standard vs SSreflect, inductifs simples vs records, classes de type vs instances canoniques, #[refine] vs Program, etc.) De plus la bibliothèque standard de Lean est vraiment beaucoup mieux faite. C'est subjectif mais je pense que la plupart des gens seront d'accord pour dire que Lean est mieux ingéniéré et a tiré des leçons de certains aspects moins bien faits de Rocq.
Comme il s'adresse largement à des matheux qui n'y connaissent rien à la logique intuitionniste, Lean n'a pas peur d'utiliser le tiers exclu, et aussi d'autres axiomes comme l'extensionnalité fonctionnelle, l'extensionnalité propositionnelle, les types quotients et l'axiome du choix. Ça n'empêche pas de raisonner sans ces axiomes en Lean, mais c'est lourdingue parce que toutes les tactiques standard les introduisent même quand elles n'en auraient pas besoin.
Rocq, en plus de permettre de faire de la théorie homotopique des types, a des options « expertes » et parfois expérimentales qui permettent de jouer avec les détails de la théorie des types, que n'a pas Lean.