Comments on Nouvelles d'octobre : covid, calculabilité, NanoPi

Ptitboul (2023-11-10T15:20:09Z)

Ta description dans "méditation sur les problèmes informatiques" m'a fait penser à une analogie avec un médecin face à un patient. Je ne sais pas si les parallèles entre l'informatique pratique et la médecine sont une tarte à la crème.

Izys (2023-10-14T15:13:58Z)

Concernant ta quête de communautés physiques de hackers, il existe d'autres organisations que les Fablabs (qui sont destinés à la fabrication d'objets) : les hackerspaces or hacklabs.

Je fréquente celui-ci, à Montreuil : [URL: https://fuz.re/ ]. En ce moment j'y suis des ateliers hebdomadaires de Rust et de Shaders en GLSL. Les mercredis soirs sont consacrés aux rencontres et blablas, un bon moment pour soumettre un problème sur lequel on coince.

J'ai conscience que Montreuil, ce n'est pas tout à fait à côté de chez toi et de ton lieu de travail. Le /tmp/lab est un peu plus près : [URL: https://www.tmplab.org/ ].

Courage pour le covid !

Natacha (2023-10-14T09:11:09Z)

J'ai fait le même constat que notre hôte sur le « méta-problème avec les problèmes informatiques », et moi aussi je me sens tellement tristement seule ces jours-ci, un contraste radical avec ma situation d'il y a vingt ans.

Je n'ai toujours pas pu déterminer si c'est moi qui ai changé (dans ces cercles sociaux moins « geeks », face à des problèmes plus compliqués à cause de ma propre montée en compétence, moins de patience face à ces problèmes, etc), si c'est le monde qui a changé (plus de silos, plus de vassalisation, plus de complexité technique, le nivellement du user-friendly sur l'expert-friendly, l'entraide comme victime collatérale de la victoire de l'open source sur le logiciel libre décrite par ploum <URL: https://ploum.net/2023-10-09-ecologie-et-opensource.html>, etc) ou une combinaison des deux.

En tout cas je rêve de pouvoir retrouver cette relation avec les problèmes informatiques (voire avec l'informatique en général), et si quelqu'un par ici a des pistes pour y arriver, je suis très intéressée par leur partage.

Bertrand (2023-10-09T20:28:54Z)

Bonjour, (première intervention sur ton blog que je suis depuis quelques temps)

Jusqu'à il y a une vingtaine d'année, donc en fait avant que je me mette au vélo pour mes déplacements, je me faisais un syndrome grippal chaque année. Depuis, plus jamais. Entre le meilleur état de santé générale, l'exposition régulière au frais / froid… et la forte baisse de fréquentation des transports en commun, je ne sais pas dire ce qui a joué.

Pour le covid, je l'ai choppé en avril 2022 et a priori ce week-end ! toux, nez qui coule énormément, grosse fatigue et nuits de merde… j'attends demain pour faire un test.

Enfin, informaticien, j'ai depuis quelques années abandonné mes séances de bidouillage des linux domestique ou des amis. Sauf nécessité perso ou requête très insistante desdits ami(e)s. Ça ne m'amuse plus, d'autant qu'au taf je gère une cinquantaines de VMs des clusters k8S… Largement de quoi me saturer du sujet.

Bon courage avec ton covid et tes préparations de cours.

Cigaes (2023-10-09T19:50:27Z)

Je pense que si tu vas sur debian-user demander « comment compiler un noyau sur Armbian (c'est pour pour le support ath9k_htc sur NanoPi R6s », tu as des chances non négligeables d'avoir une réponse.

jeanas (2023-10-09T15:04:57Z)

(Question en passant : est-ce qu'il y a un flux RSS pour ce site qui contiendrait
aussi les commentaires ?)

jeanas (2023-10-09T10:01:10Z)

@David : merci, je n'avais pas compris que Andrej Bauer, avec tous les termes techniques qu'il emploie, parlait « juste » de proof irrelevance. (Je le comprends le principe et son intérêt en pratique en Coq mais je n'ai pas étudié sérieusement la théorie derrière. D'ailleurs, il faudrait vraiment que je prenne du temps pour ça, vu qu'à l'ENS Paris-Saclay tout le monde est branché sur la preuve formelle à cause du LMF, donc ça m'arrive d'être perdu dans les discussions à ce sujet.)

> Personnellement, je n'ai pas envie de rentrer dans le débat de ce qui mérite d'être appelé « Curry-Howard », ça me semble aussi futile que de chercher à définir exactement ce qui mérite d'être appelé « transformée de Fourier » parmi les 1001 variantes de la même chose. Donc savoir si Coq relève de l'isomorphisme de Curry-Howard ou juste d'une analogie de Curry-Howard est une question qui me semble théologique et pas mathématique, et ça ne m'intéresse pas.

Tout à fait d'accord avec ça.

----

Changement partiel de sujet : il y pas mal des cours à l'ENS Paris-Saclay sur les sujets que vous allez enseigner. Je le dis juste au cas où ça vous intéresserait de regarder les documents de cours (ça peut être une source d'exercices par exemple).

- λ-calcul avec notre Jean Goubault national : https://projects.lsv.fr/agreg/?page_id=113
- Calculabilité avec le même : https://projects.lsv.fr/agreg/?page_id=312
- Projet de logique (TP en Coq entre autres) : https://lmf.cnrs.fr/AmelieLedein/ProjetLogique2023

Ruxor (2023-10-09T08:35:27Z)

@jeanas, @Thomas:

Le point soulevé par Andrej Bauer est que l'analogie entre (types,termes) et (propositions,preuves) dans Coq (et d'autres) est imparfaite parce que Coq permet (même s'il n'impose pas) l'« irrelevance des preuves », i.e., le fait que deux preuves de la même proposition soient égales, ce qui exige qu'à partir d'une preuve de ∃x.P(x) on ne puisse pas reconstruire le x qui a servi à le prouver (*même* si la logique est constructive et qu'on doit forcément établir un témoin pour y arriver, la preuve « oublie » ce témoin, ou au moins le cache et ne permet pas de le réextraire, en tout cas pas de le réextraire comme un terme), et concrètement, la règle d'élimination de ‘∃’ (qui, dans Coq, s'appelle « exists ») n'est pas la même que la règle d'élimination d'une somme (qui, dans Coq, s'appelle « sig »).

Notamment, dans Coq, on peut construire quelque chose du type suivant (qui, en notations mathématiques usuelles, convertit ∏_{x∈X} ∑_{y∈Y} Z_{x,y} en ∑_{f∈Y^X} ∏_{x∈X} Z_{x,f(x)} où ∑ désigne la réunion disjointe) :

forall X:Set, forall Y:Set, forall Z:X->Y->Set, (forall x:X, {y:Y & Z x y}) -> ({f:(X->Y) & (forall x:X, Z x (f x))}).

(“intros X Y Z H. exists (fun (x:X) => projT1 (H x)). intro x. exact (projT2 (H x)). Qed.”), mais on ne peut pas prouver son analogue exact par Curry-Howard (qui, en notations mathématiques usuelles, affirme que ∀x:X ∃y:Y P(x,y) implique ∃f:X→Y ∀x:X P(x,f(x))) :

forall X:Set, forall Y:Set, forall Z:X->Y->Prop, ((forall x:X, exists y:Y, Z x y) -> (exists f:(X->Y), forall x:X, Z x (f x))).

— parce que c'est l'axiome du choix (et, si on essaie de faire pareil en Coq, on bute sur le problème qu'il n'y a pas de « ex_projT1 »).

Indiscutablement, le fait que l'axiome du choix ne soit pas prouvable (ou pas souhaitable), c'est-à-dire qu'on ne peut pas aveuglément convertir ∀x:X ∃y:Y P(x,y) en ∃f:X→Y ∀x:X P(x,f(x))), alors qu'on peut aveuglément convertir ∏_{x∈X} ∑_{y∈Y} Z_{x,y} en ∑_{f∈Y^X} ∏_{x∈X} Z_{x,f(x)} suggère qu'il y a quelque chose qui ne tourne pas rond dans l'isomorphisme de Curry-Howard, en tout cas si on veut faire de ‘∃’ le pendant des types sommes.

A contrario, dans les théories à la Martin-Löf, l'analogie est exacte, il n'y a pas tant de ‘∃’ qu'une somme, mais la conséquence de ça est qu'on ne peut jamais se débarrasser de l'information du témoin d'existence. Et l'axiome du choix est un théorème dans ces théories, mais ça a d'autres inconvénients (l'impossibilité de réaliser correctement les quotients : chercher « setoid hell » pour une discussion).

Personnellement, je n'ai pas envie de rentrer dans le débat de ce qui mérite d'être appelé « Curry-Howard », ça me semble aussi futile que de chercher à définir exactement ce qui mérite d'être appelé « transformée de Fourier » parmi les 1001 variantes de la même chose. Donc savoir si Coq relève de l'isomorphisme de Curry-Howard ou juste d'une analogie de Curry-Howard est une question qui me semble théologique et pas mathématique, et ça ne m'intéresse pas.

Par contre, ce qui est sûr, c'est que cette subtilité sur l'élimination du ‘∃’ restera au-delà du niveau que mon collègue et moi visons d'enseigner à des élèves de 1re année d'école d'ingénieur (ce qui est différent de doctorants en logique informatique) : déjà si on arrive à communiquer l'analogie entre propositions et types au niveau propositionnel, ce n'est pas mal !

Vincent (2023-10-09T06:07:10Z)

Pour eth1/eth2, ce n'est pas tant Linux que udev qui empêche cela. La logique, c'est que le noyau peut à tout moment faire apparaître une interface avec le nom que tu voudrais utiliser et que cela rend complexe le renommage. Plutôt que de laisser l'utilisateur se tirer une balle dans le pied parce que ça marche dans 90% des cas, l'option semble désormais interdite.

jeanas (2023-10-08T23:53:09Z)

> Il semble cependant que plusieurs personnes qui connaissent le sujet considèrent que Coq (ou Lean) ne s'inscrivent pas vraiment dans le cadre de la correspondance de CH.
>
> C'est notamment ce que je comprends de la réponse d'Andrej Bauer ici https://proofassistants.stackexchange.com/a/2450/2780

Ça fait un moment que je ne me suis pas plongé dans ces trucs, il va falloir
que je révise.

> Aussi, sur l'article Wikipedia au sujet de cette correspondance, il est indiqué que les propositions existentielles y sont représentées par des paires dépendantes (sigma type), qui supposent qu'on puisse exhiber un témoin.
>
> J'ai donc du mal à comprendre comment rendre cela compatible avec l'interprétation classique du quantificateur existentiel (n'est-ce pas la limitation qu'évoque Andrej ?).

Justement, la logique de Coq est intuitionniste, pas classique. Le quantificateur existentiel
est constructif.

Ça n'empêche pas de faire de la logique
classique en Coq, on rajoute juste un axiome
"forall P: Prop, P \/ ~P". Autrement dit,
les termes peuvent contenir un terme spécial
(l'axiome) qui est supposé être du type du
tiers exclu, pour lequel il n'est pas possible
de donner un terme du calcul des constructions
inductives pures qui l'habite.

De manière plus simple, cela revient
(en théorie, pas vraiment en pratique)
à préfixer chaque théorème de
"(forall P: Prop, P \/ ~P) ->".

Je ne connais pas bien Lean mais il me
semble qu'il fait la même chose, simplement
en se préoccupant moins de faciliter les preuves
entièrement constructives (avec des
tactiques standard et une bibliothèque standard
qui n'hésitent pas à utiliser le tiers exclu).

Gabriel (2023-10-08T21:00:56Z)

Sur les tracas informatiques, je compatis. Et je vais même aller plus loin : informaticien et régulièrement en télétravail à deux pas de la butte aux cailles, je veux bien servir de cobaye pour une création de groupe de soutien dans le quartier ;-)

Thomas (2023-10-08T13:44:15Z)

@jeanas: Merci pour ces éléments de reponse.

Il semble cependant que plusieurs personnes qui connaissent le sujet considèrent que Coq (ou Lean) ne s'inscrivent pas vraiment dans le cadre de la correspondance de CH.

C'est notamment ce que je comprends de la réponse d'Andrej Bauer ici https://proofassistants.stackexchange.com/a/2450/2780

Aussi, sur l'article Wikipedia au sujet de cette correspondance, il est indiqué que les propositions existentielles y sont représentées par des paires dépendantes (sigma type), qui supposent qu'on puisse exhiber un témoin.

J'ai donc du mal à comprendre comment rendre cela compatible avec l'interprétation classique du quantificateur existentiel (n'est-ce pas la limitation qu'évoque Andrej ?).

jeanas (2023-10-08T12:32:56Z)

@Thomas :

> En tant qu'étudiant, je pense que je me demanderais tout de même quel est le lien entre ces deux sujets (théorique: lambda-calcul, typage, Curry-Howard et pratique: Coq), aborderas-tu cette question ? Si oui, je serais curieux de savoir comment…

Coq est un assistant de preuve fondé sur le calcul des constructions inductives, c'est-à-dire le calcul des constructions (un λ-calcul typé) augmenté avec des types inductifs. Une preuve Coq est un terme dans le calcul des constructions inductives, et Coq vérifie la preuve en vérifiant que le terme est bien typé. En d'autres termes, le principe même de Coq est d'utilise la correspondance de Curry-Howard.

Exemple très simple :

Goal forall P Q : Prop, P -> Q -> (P /\ Q).
Proof.
intros. split; assumption.
Show Proof.
Qed.

Ici j'ai prouvé la tautologie ∀ P Q, P ⇒ (Q ⇒ (P ∧ Q)). Avec le « Show Proof. » à la fin, il affiche

(fun (P Q : Prop)
(H : P)
(H0 : Q)
=> conj H H0)

ce qui est la représentation de la preuve comme terme du calcul des constructions inductives (conj étant le constructeur de la conjonction). Avec une notation plus standard, ce serait

λP ⋅ λQ ⋅ λH ⋅ λH' ⋅ conj H H'

Thomas (2023-10-08T08:03:47Z)

Quelqu'un saurait m'expliquer pourquoi maintenir une filière "MP Option info" et une filière MPI en parallèle ?

Sinon, tu indiques "je dois leur parler (…) un peu de l'isomorphisme de Curry-Howard (qui exprime le fait que typer un programme informatique — spécifiquement, un terme du lambda-calcul — ou vérifier une démonstration mathématique, sont en fait « la même chose »)." et "En parallèle de ça, un collègue leur fera des TP d'introduction à l'assistant de preuve Coq"

En tant qu'étudiant, je pense que je me demanderais tout de même quel est le lien entre ces deux sujets (théorique: lambda-calcul, typage, Curry-Howard et pratique: Coq), aborderas-tu cette question ? Si oui, je serais curieux de savoir comment…

Ludovic (2023-10-08T07:14:01Z)

Salut,

Pour ma part, j'ai opté pour un apu2d4 pour faire office de serveur. J'ai l'impression qu'il correspond pas mal à ce que tu veux faire sauf le chargeur non usb et une installation par port série. Par contre, j'ai bien pu mettre coreboot et une debian très classique dessus.

JMU (2023-10-07T23:49:02Z)

> Une autre chose intrigante est l'absence de contamination avérée entre le poussinet et moi.

Une copine en biologie m'avait expliqué que l'on est attiré vers des personnes ayant un système immunitaire complémentaire du sien pour des raisons de sélection naturelle, les descendants ayant une chance de combiner toutes les résistances des parents donc d'être plus viables.

Wikipedia confirme et ça a l'air solide chez les animaux (https://en.wikipedia.org/wiki/Major_histocompatibility_complex#In_sexual_mate_selection).

Par je ne ferais pas hyper confiance aux études chez les humains. Genre doi/10.1098/rspb.1995.0087 qui conclut que les filles préfèrent l'odeur des garçons avec un MHC différent, _sauf quand elles prennent la pilule_, ça ressemble à du bruit aléatoire qui est passé grâce au biais de publication. (Pourquoi la pilule renverserait le choix ? Si c'est une histoire d'hormones, a-t-on contrôlé avec la phase de cycle menstruel ? Etc.) Bon, j'ai fait dix minutes de recherche internet pour éviter de propager un ragot, ça a l'air suffisamment vrai pour poster, je vais pas faire dix heures de review de papiers de biologie.

Damien (2023-10-07T15:45:34Z)

Sur la lassitude face aux problèmes informatiques, et dans la lignée de tes nombreux billets sur Android, je n'ai également aucun regret, après 7 ans d'utilisation de CyanogenMod/LineageOS, d'être passé à un Android constructeur il y a quelques années. Quel allègement de la charge mentale, bon débarras !

Quand je gérais l'OS de mes téléphones, j'y passais aussi un temps énorme (notamment sur les mises à jour) et, malgré avoir tout essayé, je n'ai jamais eu les MMS qui fonctionnent, en émission comme en réception, un sacré comble quand j'y repense… On se moquait de moi, informaticien qui ne peut même pas utiliser les MMS…

Bref, a posteriori, je ne sais même plus vraiment pourquoi je me suis autant obstiné dans une situation où j'étais perdant sur la charge de "travail" comme sur l'utilisation au quotidien (je ne parle même pas des bugs mineurs, reboots intempestifs, etc.)

Damien (2023-10-07T11:28:52Z)

quand j'écris "fiable" à la fin, je pense au bon fonctionnement sans aller trop loin dans la bidouille (c'était très net avec Openwrt qui est beaucoup plus direct à configurer qu'un Linux classique) mais aussi au côté communautaire dont tu parles et donc de la doc, des forums, pour trouver de l'aide.

au contraire, un nano-ordinateur est générique par définition et trouver de l'aide sur des choses pointues de réseau, de wifi, etc. est hyper difficile ("on se sent seul face au problème")

Damien (2023-10-07T10:22:11Z)

Après un peu plus de réflexion sur ton billet, quelques autres choses qui me sont venues en tête :

- peut-être que l'âge a un impact sur le ressenti pénible des tracas informatique ; pour parler de mon expérience personnelle,
j'ai été chez Nerim en ADSL de 2005 à 2021, et j'ai utilisé OpenWRT, successivement avec un Netgear DG834 puis avec des TP-Link,
WR1043ND et WDR3600 les dernières années. J'ai passé des heures là-dessus et j'ai appris beaucoup de choses (notamment sur IPv6).
D'ailleurs je viens de retrouver ceci :-)
http://www.madore.org/cgi-bin/comment.pl/showcomments?href=http%3A%2F%2Fwww.madore.org%2F%7Edavid%2Fweblog%2F2011-11.html%23d.2011-11-04.1962

Le passage à la fibre a été extrêmement compliqué dans mon immeuble (je passe les détails) ; Ovh n'était pas disponible, mais vu le type de câblage,
j'ai pu souscrire simultanément un abonnement Free et un abonnement Orange (au sous sol, cela aboutit dans deux armoires distinctes),
cela fournit un premier niveau de "haute disponibilité" (il y a parfois des coupures d'un des deux lors d'un nouveau raccordement).
J'ai longuement épluché lafibre.info mais finalement j'ai décidé d'utiliser les box des opérateurs et cela fonctionne globalement bien.
Cela me libère du temps pour d'autres choses et me mets moins de pression en tant qu'"administrateur système" de la famille.
Je ne me verrais pas du tout revenir en arrière, peut-être parce que j'ai vieilli…

De plus, vu que j'ai un métier technique dans l'infra, je passe déjà toutes mes journées sur des problèmes informatiques à résoudre (là-dessus
c'est différent de toi) et cela a nettement réduit mon appétence et ma patience pour y consacrer plein de temps et de frustration
sur mon temps personnel.

- je me demande si tes ennuis de "box" ne sont pas surtout liés au fait que tu as choisi (tu ne dis pas vraiment pourquoi : coût, "mode", autre?) des nano-ordinateurs
comme équipement réseau principal. Vu ce que j'ai écrit au dessus, je ne suis pas à jour sur le sujet mais les gens qui continuent à gérer
leur box eux-même avec la fibre me semblent principalement utiliser des équipements des marques :
* Turris : https://www.turris.com/en/products/omnia/
* Ubiquiti mais leurs modèles "EdgeRouter" appréciés des bidouilleurs ne semblent plus exister, remplacés par quelque chose qui semble beaucoup plus fermé
https://ui.com/us/consoles
* Mikrotik https://mikrotik.com/product/rb5009ug_s_in

comme je ne suis pas à jour, je ne sais pas dans quelle mesure chacun est customisable et si on peut installer des distributions alternatives ;
mais choisir ce type d'équipement me semblerait plus "fiable" pour faire du réseau qu'un nano-ordinateur "générique"…

a3nm (2023-10-07T03:21:54Z)

> je me dis que ce dont j'ai besoin quand je rencontre des problèmes lors de bidouilles informatiques, ce n'est pas de l'aide au sens de quelqu'un qui s'y connaîtrait très bien et qui me donnerait des réponses, mais plutôt le support émotionnel de quelqu'un qui écouterait le récit de mes problèmes, accepterait de s'intéresser au contexte précis, m'apporterait des suggestions occasionnelles sur comment il s'y prendrait, et surtout m'aiderait à traverser cette épreuve de patience

J'ai l'impression que beaucoup de gens utilisent ChatGPT précisément pour ça !

Damien (2023-10-06T19:54:11Z)

Il y a quelques années, il y a eu une "mode" (façon de parler) des Fablab. On en entend plus trop parler donc je ne sais pas si c'est devenu moins nouveau ou si ça a juste fermé car trop peu de personnes intéressées ou de revenus pour les faire fonctionner (j'ai l'impression que certains étaient associatifs alors que d'autres étaient en arrière plan des entreprises, qui n'ont peut être pas perduré).

Bien sûr c'était assez large (électronique, impression 3D…) mais pas mal insistaient aussi sur des séances de bidouille autour de Linux.