En principe, une démonstration mathématique ne fait que suivre des règles logiques bien définies, et devrait donc pouvoir être encodée informatiquement et vérifiée par un ordinateur. Où en est-on dans la pratique et dans la théorie ? Petit tour au pays des assistants de preuve, des langages de programmation dédiés aux démonstrations, et de leur fondement théorique le plus commun, la théorie des types.
Journal Mon inquiétude sur les dépendances en Rust

Bonjour 'Nal,
Tout a commencé quand j'ai voulu faire des choses un peu inhabituelles sur mon blog personnel (entre autres, écrire des maths avec une syntaxe personnalisée), et pour cela changer le moteur de blog. De Zola, un générateur de site statique dans la lignée de Jekyll, Hugo, etc., je suis passé à un petit script maison. J'ai décidé de l'écrire en Rust, car même si ce n'est pas le plus pratique comme langage de script, c'est un langage (…)
Journal Le marketing des logiciels, épisode 20240410

Bonjour 'Nal,
Un court journal aujourd'hui pour ranter sur le marketing des logiciels et plateformes logicielles. Exemple du jour : Netlify.
J'en entends parler, j'essaie de comprendre ce que c'est (je n'y connais rien en développement Web). Logiquement, je vais sur https://www.netlify.com. Voilà ce que je lis :
« Connect everything. Build anything. Netlify is the essential platform for the delivery of exceptional and dynamic web experiences, without limitations. »
« Netlify Composable Web Platform. Streamlined orchestration, simplified and (…)
Journal Mon gestionnaire de mots de passe, en 50 lignes de HTML

Bonjour « Nal » (d'où vient cette tradition ?),
Comme chacun de nous, j'ai plus d'une centaine de mots de passe pour divers sites, certains très sensibles, par exemple ceux de mon Webmail, des impôts ou de ma mutuelle, et d'autres dont je ne serais même pas gêné qu'ils soient publics, comme sur tous ces sites insupportables qui exigent de créer un compte pour la moindre petite action, même s'il y a de fortes chances que je n'utilise plus jamais (…)
L'installation et la distribution de paquets Python (2/4)
Cette dépêche est la deuxième d’une série de quatre sur le packaging en Python :
- L’histoire du packaging Python
- Tour de l’écosystème actuel
- Le casse-tête du code compilé
- La structure de la communauté en question
Je vais donc proposer un aperçu plus ou moins complet des différents outils, et de ce qu’ils font ou ne font pas, en essayant de les comparer. Mais je parlerai aussi des fichiers de configuration, des dépôts où les paquets sont publiés, des manières d’installer Python lui-même, et de l’interaction de tout ceci avec les distributions Linux. En revanche, je laisse de côté pour l’instant les paquets écrits en C, C++ ou Rust et la complexité qu’ils apportent.
L’installation et la distribution de paquets Python (1/4)
Quelques dépêches précédentes ont parlé des outils de packaging Python, comme ici, là ou encore là. Je vais chercher à faire un tour complet de la question, non seulement du point de vue de l’utilisateur qui cherche à comprendre quelle est « la bonne » solution (← ha ha ha rire moqueur…), mais aussi en expliquant les choix qui ont été faits, les évolutions, la structure de la communauté autour des outils, et les critiques qui leur sont souvent adressées, à tort ou à raison.