Dans le cadre de mon taf, je fais un peu de veille sur le monde de l'informatique, donc je me dis que je peux aussi en parler ici.

Et on commence par un bug, trouvé il y a quelques heures, qui affecte Firefox, et plus particulièrement le protocole HTTP/3. Si votre navigateur est configuré pour utiliser automatiquement des services en HTTP/3, le bug sera déclenché plus rapidement (par exemple DoH ou la télémétrie). Ce bug fait tourner Firefox en boucle et le rend inutilisable, y compris la partie qui s'occupe d'en faire les mises à jour automatique.

Si vous êtes affecté.e.s, le plus simple est de désactiver HTTP/3 : aller dans about:config, chercher la clé 'network.http.http3.enabled', et la mettre à False.

Bien entendu, les conséquences pour le navigateur risquent d'être gigantesques, sachant qu'il est déjà en perte de vitesse.

Source

S'il y a des gens que ça intéresse, je signale que comme on est en décembre, l'Advent of code a repris.

Voir ici

Il s'agit d'un challenge avec un défi de programmation par jour. Les problèmes sont de difficulté croissante. Généralement, des gens qui débutent peuvent faire les 10 premiers jours sans trop de difficulté (même si des astuces peuvent aider, bien sûr). Les prérequis sont par contre de savoir lire et parser un fichier ou une chaine de caractères.

Allez aujourd'hui je vous parle d'un truc que j'aime bien et qui est très niche dans la galaxie informatique : les méthodes formelles. C'est souvent considéré soit comme un truc très obscur, soit réservé à un nombre très restreint de personnes dans l'industrie, et ça a du sens.

On parle de méthodes formelles pour une manière de programmer pour laquelle on prouve que ce qu'on a programmé correspond bien à ce qu'on veut.

Ça peut sembler un peu superflu parce que "on voit bien ce qu'on écrit quand même" (et si vous faites le concours ci-dessus, par exemple, c'est à peu près clair que vous allez pas vous emmerder à prouver que ce que vous codez est correct), mais c'est bien ça le problème : quand on code, parfois on veut garantir l'absence absolue de bug, et les méthodes classiques de programmation ne permettent pas d'atteindre ça.

Pour prendre un exemple un peu neutre, imaginons que vous écriviez le programme d'un feu rouge, et détaillons les différentes étapes :

A/ Le repli

La première chose à voir, c'est que vous avez un état de repli, c'est-à-dire qu'en cas de problème, basculer vers cet état garantit la sécurité. Dans le cas de votre feu rouge, c'est juste de s'éteindre parce que le code de la route prend alors la relève et donne les priorités sur votre intersection. Avantage : cet état de repli ne nécessite pas d'alimentation électrique non plus, donc pas besoin de la garantir en sécurité. En fonction du logiciel sur lequel vous travaillez, l'état de repli est plus ou moins complexe à atteindre. Un autre exemple simple, c'est un train : l'état de repli c'est de freiner (et si vous mettez un coup de hache dans l'ordi de bord d'un train, il va effectivement se mettre à freiner). Un exemple complexe, c'est un avion : le repli c'est de se poser sur une piste d'aterrissage. Pour ça il faut garantir que les calculateurs de bord soient alimentés électriquement en permanence (pas de manœuvre manuelle possible).

B/ La conception

Quand vous allez programmer votre feu rouge, vous allez décider des cycles, des synchronisations, et des mécanismes d'action quand quelqu'un appuie sur le bouton d'appel piéton. Problème : pourquoi est-ce que ce que vous décrivez est sûr ? N'est-il pas possible que deux routes perpendiculaires aient un feu vert en même temps ? Idéalement, on voudrait à cette étape garantir l'absence d'accident de voiture si tout se passe correctement. Un bon moyen d'éviter une situation, c'est d'écrire directement dans la conception que le système doit passer en repli si une situation anormale est observée.

Ici, les méthodes formelles permettent de prouver la fiabilité d'un système, à condition de le modéliser entièrement (il faut modéliser les humains et leur fonctionnement). Dans le cas d'un feu rouge, on voudra sans doute modéliser le temps maximum que met un.e piéton.ne ou une voiture à libérer la chaussée. Dans le ferroviaire, il faut modéliser les trains, leur vitesse, les procédures que connaissent les conducteurs et les agents de postes d'aiguillages, etc.

La conception prouvée par méthodes formelles est encore à un niveau balbutiant, mais il y a des progrès importants dessus dans l'industrie.

(Je tâcherai de faire plus tard :
C/ Le développement
D/ La compilation
E/ L'exécution
F/ La validation de données)