Aujourd'hui, beaucoup de sites utilisent des certificats à durée de vie relativement longue, typiquement un an, obtenus de la part du registrar DNS, et renouvelés à la main en demandant un nouveau certificat au registrar et en uploadant le fichier qu'on obtient sur le serveur. Pour eux, ce ne sera plus vraiment tenable, s'il faut faire cette manip tous les mois, donc tout le monde va devoir basculer sur l'autre méthode, celle du renouvellement automatique, qui est déjà très commune parce que Let's Encrypt, la principale autorité de certification à être gratuite, ne fournit déjà que des certificats à durée de vie assez courte.
(Moi, ça m'embête un peu, parce que les outils de renouvellement automatique comme acme.sh et Certbot m'ont causé quelques misères. J'espère que ce sera plus au point pour mes usages d'ici-là.)
C'est une délibération du CA/Browser Forum, un consortium qui rassemble la plupart des navigateurs Web et des autorités de certification qui délivrent les certificats TLS (que tout le monde continue d'appeler SSL), plus quelques autres.
Cette décision signifie donc probablement que presque toutes les CAs vont réduire la durée de validité maximale de leurs certificats, et que les navigateurs vont se mettre à refuser les certificats avec des durées plus longues.
$ host linuxfr.org
linuxfr.org has address 213.36.253.103
linuxfr.org mail is handled by 50 main.linuxfr.org.
Le serveur de linuxfr.org est joignable à l'adresse IP 213.36.253.103. Pourtant, comme vous l'avez constaté sur d'autres sites, si on essaie de joindre https://213.36.253.103 sans précaution, on n'obtient pas la page d'accueil de LinuxFR. On peut reproduire dans un terminal avec curl ce que fait un navigateur :
$ curl --insecure https://213.36.253.103
<!DOCTYPE html>
<!-- Managed by Ansible, do not edit by hand -->
<html lang="fr">
<head>
<meta charset="utf-8">
<title>Serveur oups.linuxfr.org - LinuxFr.org</title>
</head>
<body><h1>Serveur oups.linuxfr.org - LinuxFr.org</h1>
<p>Si vous êtes arrivé(e) sur cette page, c'est probablement parce que vous kiffez l'HTML 2.</p>
</body>
</html>
La raison à ceci est qu'un même serveur peut, sur une même IP, servir plusieurs sites Web différents. Quand il reçoit une connexion HTTP, il a besoin de savoir à quel site elle se rapporte. Or notre requête ne lui fournit pas cette information. Dans le protocole HTTP, elle est donnée dans l'en-tête Host, qu'on peut demander à curl d'envoyer comme ceci :
Maintenant, il faut que j'explique pourquoi on a eu besoin de --insecure. Dans le bon vieux temps, les requêtes étaient faites en HTTP simple, et le Host suffisait. Mais est arrivé le HTTPS, qui rajoute une couche de chiffrement TLS par dessus le HTTP. Or, dans le début de la connexion TLS, avant même que des données soient transmises, le client est censé vérifier que le serveur a fourni un certificat, qui atteste qu'il est bien le serveur qu'il prétend être. Donc, si un serveur propose plusieurs sites, quand il reçoit une requête, il ne pouvait pas encore savoir quel site voulait le client, et devait forcément fournir un certificat valide pour tous les sites possibles. Le hic, c'est qu'il peut être compliqué, et un peu moins sécurisé aussi, d'obtenir un tel certificat. Pour pallier ce manque est arrivée la SNI, « Server Name Indication », une extension du protocole TLS qui permet au client de spécifier quel site il veut dès le début de la connexion TLS. Avec la commande ci-dessus, curl passe le Host mais pas la SNI, donc se plaint légitimement qu'il n'a pas de certificat valide pour 213.36.253.103 car le certificat envoyé par le serveur de LinuxFR n'est valide que pour linuxfr.org (et j'ai mis le --insecure pour lui demander de l'ignorer).
curl n'a apparemment pas d'option pour régler manuellement le SNI, donc je ne peux pas terminer l'exemple aussi pédagogiquement que je le voudrais, mais dans la requête curl https://linuxfr.org, il utilise l'URL non seulement pour trouver l'IP 213.36.253.103 via DNS, mais aussi pour régler le SNI dans la connexion TLS et le Host dans la connexion HTTP qu'elle chiffre.
« the Commission will prioritise […] the preparation of a Technology Roadmap on encryption, to identify and assess technological solutions that would enable law enforcement authorities to access encrypted data in a lawful manner, safeguarding cybersecurity and fundamental rights. »
En pratique, mes mots de passe sont enregistrés dans Firefox Sync, donc la plupart du temps je n'ai pas besoin d'ouvrir mon gestionnaire de mots de passe parce qu'ils sont préremplis par la complétion built-in de Firefox.
Quand je veux mon mot de passe pour un service qui n'est pas sur le Web (ma boîte mail, etc.), j'ouvre mon gestionnaire, je rentre le nom du service et mon mot de passe maître, et ça me donne mon mot de passe. Et quand je veux créer un nouveau mot de passe pour n'importe quoi, je l'ouvre aussi et je laisse Firefox l'enregistrer. Et comme noté sur la page du générateur, ça se fait très facilement en ligne de commande aussi.
Donc pour résumer, l'autoremplissage est fourni par Firefox, la synchronisation aussi (Firefox Sync, qui est associé à ton compte Mozilla), et la sûreté contre une panne des services Mozilla + possibilité de retrouver très facilement un mot de passe sur un autre ordinateur que le sien + possibilité de retrouver un mot de passe en ligne de commande et même sans réseau sont fournies par le générateur ultra-simple.
Mon PC actuel ainsi que ceux de ma sœur et mon frère (convertis à Linux par moi) sont achetés sur https://laptopwithlinux.com. J'ai trouvé ça très pratique : plutôt que de lire les specs de zillions de modèles différents, tu as un formulaire à remplir où tu choisis entre plusieurs options le processeur, la taille de RAM, la distribution Linux à préinstaller, la disposition de clavier à imprimer sur les touches, etc., ils l'assemblent et ils te l'expédient. J'en suis très satisfait jusqu'ici.
Je n'ai pas vérifié la configuration de ce réseau (je peux essayer de le faire), mais comme NetworkManager manifestement demande une IPv4 par DHCP et ne l'obtient pas, je ne crois pas que ce soit juste désactivé à son niveau…
Non, le problème ne se produit pas quand elle se connecte directement à la Livebox, seulement sur le répéteur.
Je n'ai pas non plus regardé les autres appareils de mes propres yeux mais elle dit qu'ils fonctionnent bien avec le Wifi du répéteur (en plus de bien fonctionner en mobile et sur le Wifi de la Livebox). Et il n'y a aucun VPN dans l'histoire.
Tu serais surpris de ce qui peut sortir même de chez Google. D'accord, le crawler de Google Search est probablement bon. Mais il y a deux ans, SourceHut a dû menacer de blacklister les serveurs de Google qui maintiennent le cache des paquets Go, parce que ces serveurs mettaient SourceHut sous un quasi-DDoS en faisant des git clone complets (alors qu'il n'en avaient pas besoin), indépendamment sans se coordonner entre eux. Apparemment le même dépôt pouvait se retrouver cloné 2000 fois par jour !
Je ne prétends pas débattre avec le niveau requis, mais peut on encore parler de démonstration quand c'est "trivial" et que cela tient en une ligne ?
Oui, pourquoi pas ? De même que les maths ont fait un bond en avant quand zéro a été reconnu comme un vrai nombre, la logique marche mieux quand on reconnaît aussi les démonstrations triviales comme de vraies démonstrations :-)
De ce que je comprends il y a une sorte de consensus qui considère que les preuves formelles n'ont pas besoin d'aller au delà d'un certain niveau de détail. Les résultats "triviaux" n'ont pas à être démontrés et peuvent simplement être placés dans une bibliothèque.
Je ne sais pas d'où tu tires cette impression mais soit j'ai mal compris ce que tu veux dire, soit c'est faux.
C'est quand même un peu le but de la preuve formelle que tout soit fait dans tous les détails y compris triviaux. Bien sûr, quand on est en plein développement, on peut laisser des lemmes triviaux comme admis pour les prouver plus tard, et il peut arriver qu'on les garde non prouvés dans le résultat fini, mais ce n'est pas commun (et quand c'est le cas, ça va normalement être mentionné explicitement).
Les projets de formalisation réussis que j'ai mentionnés (retournement de la sphère, etc.) n'utilisent aucun lemme admis (seulement des axiomes « logiques » comme le tiers exclu).
Et cette preuve « rfl » de 2+2=4 (plus généralement de l'égalité entre deux termes définitionnellement égaux) est bien une preuve, pas un appel à un lemme admis.
Notons tout de même que l'automatisation se développe énormément, d'abord la théorie des types en contient intrinsèquement une dose (l'égalité définitionnelle), ensuite Rocq comme Lean (et sûrement Agda, mais je connais moins bien) ont des tactiques qui font de la recherche automatique de preuve, et Lean a une tactique « simpl » très appréciée pour simplifier toutes sortes de buts. De manière plus générale, Rocq et Lean ont de grosses bibliothèques de tactiques (voir p.ex. https://rocq-prover.org/doc/V8.20.0/refman/coq-tacindex.html) pour faire plein d'étapes de preuve à la fois.
Par exemple, la preuve de 2+2=4 en Lean est triviale (c'est un exemple d'égalité définitionnelle) :
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.
(Mais comme je l'évoque dans le billet, le ministre a aussi évoqué le terrorisme et la pédophilie, parce qu'il ne faudrait quand même pas oublier les bonnes vieilles recettes de grand-mère.)
Comme me l'a fait remarquer Patrick Massot, la ligne
Lean, créé par Leonardo de Moura et développé depuis 2013 chez Microsoft Research, écrit en C++, placé sous licence Apache 2.0.
contient des infos obsolètes : Leonardo de Moura ne travaille plus chez Microsoft Research, et contrairement à Lean 3, Lean 4 est principalement écrit en Lean 4 (je n'ai pas regardé comment c'était bootstrappé).
Est-ce qu'un modérateur voudrait bien corriger ça ? Merci !
Je ne suis pas développeur moi-même, pourtant je certifie que je passe énormément de temps à découvrir des bugs dans l'intranet de mon école, dans mon émulateur de terminal, dans Firefox, … 🙂 Certes, ce n'est pas moi qui écris les tests. Mais si un modérateur passe par là, on pourrait effectivement changer ça en « tous les développeurs (voire les autres !) passent … »
Entre ce journal, celui-là, celui-là, celui-là et maintenant celui-ci, vous faites un concours du journal le plus moinssé ? Le plus pédant ? Le plus hors-sujet ? Faites un petit effort, merci.
Armin Ronacher et Drew DeVault ont tous les deux écrit des billets de blog sur le marché des imprimantes 3D (je ne suis pas forcément d'accord, je pointe juste qu'ils sont intéressants) :
[^] # Re: Des explications ?
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Réduction de la durée maximale de validité des certificats de 398 à 47 jours approuvée. Évalué à 6 (+4/-0).
Aujourd'hui, beaucoup de sites utilisent des certificats à durée de vie relativement longue, typiquement un an, obtenus de la part du registrar DNS, et renouvelés à la main en demandant un nouveau certificat au registrar et en uploadant le fichier qu'on obtient sur le serveur. Pour eux, ce ne sera plus vraiment tenable, s'il faut faire cette manip tous les mois, donc tout le monde va devoir basculer sur l'autre méthode, celle du renouvellement automatique, qui est déjà très commune parce que Let's Encrypt, la principale autorité de certification à être gratuite, ne fournit déjà que des certificats à durée de vie assez courte.
(Moi, ça m'embête un peu, parce que les outils de renouvellement automatique comme acme.sh et Certbot m'ont causé quelques misères. J'espère que ce sera plus au point pour mes usages d'ici-là.)
[^] # Re: Des explications ?
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Réduction de la durée maximale de validité des certificats de 398 à 47 jours approuvée. Évalué à 8 (+6/-0).
C'est une délibération du CA/Browser Forum, un consortium qui rassemble la plupart des navigateurs Web et des autorités de certification qui délivrent les certificats TLS (que tout le monde continue d'appeler SSL), plus quelques autres.
Cette décision signifie donc probablement que presque toutes les CAs vont réduire la durée de validité maximale de leurs certificats, et que les navigateurs vont se mettre à refuser les certificats avec des durées plus longues.
# En-tête Host et SNI
Posté par jeanas (site web personnel, Mastodon) . En réponse au message [Résolu] Questions protocoles Internet (IP & RTSP). Évalué à 10 (+8/-0). Dernière modification le 08 avril 2025 à 12:23.
Bonjour,
Prenons un exemple avec des requêtes à LinuxFR.
Le serveur de
linuxfr.orgest joignable à l'adresse IP 213.36.253.103. Pourtant, comme vous l'avez constaté sur d'autres sites, si on essaie de joindre https://213.36.253.103 sans précaution, on n'obtient pas la page d'accueil de LinuxFR. On peut reproduire dans un terminal aveccurlce que fait un navigateur :La raison à ceci est qu'un même serveur peut, sur une même IP, servir plusieurs sites Web différents. Quand il reçoit une connexion HTTP, il a besoin de savoir à quel site elle se rapporte. Or notre requête ne lui fournit pas cette information. Dans le protocole HTTP, elle est donnée dans l'en-tête
Host, qu'on peut demander àcurld'envoyer comme ceci :Maintenant, il faut que j'explique pourquoi on a eu besoin de
--insecure. Dans le bon vieux temps, les requêtes étaient faites en HTTP simple, et leHostsuffisait. Mais est arrivé le HTTPS, qui rajoute une couche de chiffrement TLS par dessus le HTTP. Or, dans le début de la connexion TLS, avant même que des données soient transmises, le client est censé vérifier que le serveur a fourni un certificat, qui atteste qu'il est bien le serveur qu'il prétend être. Donc, si un serveur propose plusieurs sites, quand il reçoit une requête, il ne pouvait pas encore savoir quel site voulait le client, et devait forcément fournir un certificat valide pour tous les sites possibles. Le hic, c'est qu'il peut être compliqué, et un peu moins sécurisé aussi, d'obtenir un tel certificat. Pour pallier ce manque est arrivée la SNI, « Server Name Indication », une extension du protocole TLS qui permet au client de spécifier quel site il veut dès le début de la connexion TLS. Avec la commande ci-dessus,curlpasse leHostmais pas la SNI, donc se plaint légitimement qu'il n'a pas de certificat valide pour213.36.253.103car le certificat envoyé par le serveur de LinuxFR n'est valide que pourlinuxfr.org(et j'ai mis le--insecurepour lui demander de l'ignorer).curln'a apparemment pas d'option pour régler manuellement le SNI, donc je ne peux pas terminer l'exemple aussi pédagogiquement que je le voudrais, mais dans la requêtecurl https://linuxfr.org, il utilise l'URL non seulement pour trouver l'IP 213.36.253.103 via DNS, mais aussi pour régler le SNI dans la connexion TLS et leHostdans la connexion HTTP qu'elle chiffre.Sur Wikipédia : https://en.wikipedia.org/wiki/List_of_HTTP_header_fields#Standard_request_fields et https://en.wikipedia.org/wiki/Server_Name_Indication
HTH
[^] # Re: J'en ai déjà parlé ici
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Comment gérez-vous vos mots de passe (et l’autoremplissage des formulaires) ?. Évalué à 3 (+1/-0).
Pour ma part, je ne stocke mon mot de passe maître que dans ma tête.
# L'extrait pertinent
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien La commission européenne veut *encore* casser le chiffrement de bout en bout des messageries. Évalué à 10 (+8/-0).
« the Commission will prioritise […] the preparation of a Technology Roadmap on encryption, to identify and assess technological solutions that would enable law enforcement authorities to access encrypted data in a lawful manner, safeguarding cybersecurity and fundamental rights. »
# J'en ai déjà parlé ici
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Comment gérez-vous vos mots de passe (et l’autoremplissage des formulaires) ?. Évalué à 8 (+6/-0).
https://linuxfr.org/users/jeanas/journaux/mon-gestionnaire-de-mots-de-passe-en-50-lignes-de-html
En pratique, mes mots de passe sont enregistrés dans Firefox Sync, donc la plupart du temps je n'ai pas besoin d'ouvrir mon gestionnaire de mots de passe parce qu'ils sont préremplis par la complétion built-in de Firefox.
Quand je veux mon mot de passe pour un service qui n'est pas sur le Web (ma boîte mail, etc.), j'ouvre mon gestionnaire, je rentre le nom du service et mon mot de passe maître, et ça me donne mon mot de passe. Et quand je veux créer un nouveau mot de passe pour n'importe quoi, je l'ouvre aussi et je laisse Firefox l'enregistrer. Et comme noté sur la page du générateur, ça se fait très facilement en ligne de commande aussi.
Donc pour résumer, l'autoremplissage est fourni par Firefox, la synchronisation aussi (Firefox Sync, qui est associé à ton compte Mozilla), et la sûreté contre une panne des services Mozilla + possibilité de retrouver très facilement un mot de passe sur un autre ordinateur que le sien + possibilité de retrouver un mot de passe en ligne de commande et même sans réseau sont fournies par le générateur ultra-simple.
# laptopwithlinux.com
Posté par jeanas (site web personnel, Mastodon) . En réponse au message Achat d'un ordinateur - les sites qui vendent des ordinateur avec linux pré-installer. Évalué à 2 (+0/-0). Dernière modification le 03 avril 2025 à 23:23.
Mon PC actuel ainsi que ceux de ma sœur et mon frère (convertis à Linux par moi) sont achetés sur https://laptopwithlinux.com. J'ai trouvé ça très pratique : plutôt que de lire les specs de zillions de modèles différents, tu as un formulaire à remplir où tu choisis entre plusieurs options le processeur, la taille de RAM, la distribution Linux à préinstaller, la disposition de clavier à imprimer sur les touches, etc., ils l'assemblent et ils te l'expédient. J'en suis très satisfait jusqu'ici.
# Super offre ! Mais…
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Nouvelle typologie de comptes LinuxFr.org : segmentation et enrichissement de notre offre. Évalué à 9 (+7/-0). Dernière modification le 01 avril 2025 à 23:22.
… il manque un dernier point pour que les comptes Premium soient vraiment la classe : compléter
par
----------> []
[^] # Re: idées
Posté par jeanas (site web personnel, Mastodon) . En réponse au message Répéteur Wifi qui refuse de fournir une adresse IPv4 par DHCP. Évalué à 2 (+0/-0). Dernière modification le 30 mars 2025 à 18:20.
Je n'ai pas vérifié la configuration de ce réseau (je peux essayer de le faire), mais comme NetworkManager manifestement demande une IPv4 par DHCP et ne l'obtient pas, je ne crois pas que ce soit juste désactivé à son niveau…
Non, le problème ne se produit pas quand elle se connecte directement à la Livebox, seulement sur le répéteur.
Je n'ai pas non plus regardé les autres appareils de mes propres yeux mais elle dit qu'ils fonctionnent bien avec le Wifi du répéteur (en plus de bien fonctionner en mobile et sur le Wifi de la Livebox). Et il n'y a aucun VPN dans l'histoire.
[^] # Re: vibe coding
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Le site de curl désormais à 1,6 Go/minute de trafic à cause des crawlers pour LLMs. Évalué à 6 (+4/-0). Dernière modification le 28 mars 2025 à 16:29.
Tu serais surpris de ce qui peut sortir même de chez Google. D'accord, le crawler de Google Search est probablement bon. Mais il y a deux ans, SourceHut a dû menacer de blacklister les serveurs de Google qui maintiennent le cache des paquets Go, parce que ces serveurs mettaient SourceHut sous un quasi-DDoS en faisant des
git clonecomplets (alors qu'il n'en avaient pas besoin), indépendamment sans se coordonner entre eux. Apparemment le même dépôt pouvait se retrouver cloné 2000 fois par jour !# Précédemment
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Le site de curl désormais à 1,6 Go/minute de trafic à cause des crawlers pour LLMs. Évalué à 5 (+3/-0).
https://linuxfr.org/users/vendrediouletrollsauvage/liens/les-infrastructures-du-libre-attaquees-par-des-entreprises-de-l-ia
[^] # Re: Preuves de programme et preuves de théorèmes
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 (+2/-0).
Oui, pourquoi pas ? De même que les maths ont fait un bond en avant quand zéro a été reconnu comme un vrai nombre, la logique marche mieux quand on reconnaît aussi les démonstrations triviales comme de vraies démonstrations :-)
Je ne sais pas d'où tu tires cette impression mais soit j'ai mal compris ce que tu veux dire, soit c'est faux.
C'est quand même un peu le but de la preuve formelle que tout soit fait dans tous les détails y compris triviaux. Bien sûr, quand on est en plein développement, on peut laisser des lemmes triviaux comme admis pour les prouver plus tard, et il peut arriver qu'on les garde non prouvés dans le résultat fini, mais ce n'est pas commun (et quand c'est le cas, ça va normalement être mentionné explicitement).
Les projets de formalisation réussis que j'ai mentionnés (retournement de la sphère, etc.) n'utilisent aucun lemme admis (seulement des axiomes « logiques » comme le tiers exclu).
Et cette preuve « rfl » de 2+2=4 (plus généralement de l'égalité entre deux termes définitionnellement égaux) est bien une preuve, pas un appel à un lemme admis.
[^] # Re: Preuves de programme et preuves de théorèmes
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é à 2 (+0/-0). Dernière modification le 24 mars 2025 à 17:45.
Notons tout de même que l'automatisation se développe énormément, d'abord la théorie des types en contient intrinsèquement une dose (l'égalité définitionnelle), ensuite Rocq comme Lean (et sûrement Agda, mais je connais moins bien) ont des tactiques qui font de la recherche automatique de preuve, et Lean a une tactique « simpl » très appréciée pour simplifier toutes sortes de buts. De manière plus générale, Rocq et Lean ont de grosses bibliothèques de tactiques (voir p.ex. https://rocq-prover.org/doc/V8.20.0/refman/coq-tacindex.html) pour faire plein d'étapes de preuve à la fois.
Par exemple, la preuve de 2+2=4 en Lean est triviale (c'est un exemple d'égalité définitionnelle) :
[^] # 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 (+2/-0).
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.
[^] # Re: Ne pas confondre
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien [Mon blog] Recherche adultes pour empêcher le gouvernement de casser Internet. Évalué à 4 (+2/-0).
(Mais comme je l'évoque dans le billet, le ministre a aussi évoqué le terrorisme et la pédophilie, parce qu'il ne faudrait quand même pas oublier les bonnes vieilles recettes de grand-mère.)
# Ce n'est pas nouveau (mais ça reste d'actualité)
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Des chefs de polices EU demandent aux gouvernement d'agir contre le chiffrement des comm. (2024/09). Évalué à 4 (+2/-0).
Déjà posté ici à l'époque : https://linuxfr.org/users/glandos/liens/europol-s-oppose-aux-messageries-chiffrees
# Petite rectification
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é à 2 (+0/-0).
Comme me l'a fait remarquer Patrick Massot, la ligne
contient des infos obsolètes : Leonardo de Moura ne travaille plus chez Microsoft Research, et contrairement à Lean 3, Lean 4 est principalement écrit en Lean 4 (je n'ai pas regardé comment c'était bootstrappé).
Est-ce qu'un modérateur voudrait bien corriger ça ? Merci !
[^] # Re: Clichés
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é à 2 (+0/-0).
Merci !
[^] # Re: Clichés
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 (+2/-0).
Je ne suis pas développeur moi-même, pourtant je certifie que je passe énormément de temps à découvrir des bugs dans l'intranet de mon école, dans mon émulateur de terminal, dans Firefox, … 🙂 Certes, ce n'est pas moi qui écris les tests. Mais si un modérateur passe par là, on pourrait effectivement changer ça en « tous les développeurs (voire les autres !) passent … »
[^] # Re: Pour la complétude, j'ajoute le couple SPARK/Ada
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é à 3 (+1/-0).
Oui, voilà, ça m'a l'air d'être de la logique de Hoare, pas de la théorie des types.
[^] # Re: Il y a du contexte?
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Wikipédia:Lettre ouverte : non à l'intimidation des contributeurs bénévoles. Évalué à 5 (+3/-0).
La pétition demande d'être autoconfirmé (automatique au bout de quelques jours), pas autopatrouillé.
# Qu'est-ce qui se passe en ce moment ?
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal HS : La "théorie du clan primal" vu par mon ami virtuel . Évalué à 8 (+7/-0).
Entre ce journal, celui-là, celui-là, celui-là et maintenant celui-ci, vous faites un concours du journal le plus moinssé ? Le plus pédant ? Le plus hors-sujet ? Faites un petit effort, merci.
# Liens
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Alors ? Vous êtes content de votre imprimante Bambu Lab ?!. Évalué à 3 (+2/-0).
Armin Ronacher et Drew DeVault ont tous les deux écrit des billets de blog sur le marché des imprimantes 3D (je ne suis pas forcément d'accord, je pointe juste qu'ils sont intéressants) :
https://lucumr.pocoo.org/2023/12/25/life-and-death-of-open-source/
https://drewdevault.com/2023/12/26/2023-12-26-Prusa-is-floundering.html
# Mise à jour
Posté par jeanas (site web personnel, Mastodon) . En réponse au journal Pas de milliardaires au FOSDEM. Évalué à 4 (+3/-0). Dernière modification le 20 janvier 2025 à 15:00.
DeVault a écrit un nouveau billet de blog pour s'expliquer davantage : https://drewdevault.com/2025/01/20/2025-01-20-FOSDEM-protest.html
[^] # Re: bloub
Posté par jeanas (site web personnel, Mastodon) . En réponse au lien Ed Zitron sur la merdification. Évalué à 1.
Ah, désolé, je ne l'avais pas vu passer.