Blackknight a écrit 1237 commentaires

même s'il n'a pas été écrit à la main, mais généré à partir d'un langage plus haut niveau

De mémoire, il s'agit de la Méthode B et l'outil qui était utilisé était l'Atelier B.
A l'époque, c'était Matra Transport International qui avait effectué une partie du boulot et du coup chez Matra Systèmes & Information où je bossais, des collègues l'avaient aussi utilisé pour un autre projet.
Je me souviens que cela ne semblait pas évident du tout :D

Ce type de technique se retrouve dans les solveurs SMT (Satisfiability modulo theories), comme par exemple l'outil alt-ergo (écrit en OCaml) utilisé, entre autre, par Spark dont a parlé Blackknight.

Spark utilise aussi les SMT Z3 et CVC4 écrits tout deux en C++.
Par contre, j'avoue que je n'y connais rien et que je ne fais qu'utiliser, mon niveau de math étant bien en-deça du pré-requis ;)

mais c'est vieux et plus personne n'a envie de faire de XML.

C'est moins vieux que le C++ ;)

Mais comme il a été dit plus haut, ces formats s'intéressent autant à la forme qu'au fond (voire plus ?).

Enfin, n'allez pas croire que je sois un fan du XML, loin s'en faut mais il s'agit là pour moi d'un des usages les plus intéressants.

DocBook permet vraiment de gérer de grosses bases de documentation et de faire du vrai hypertexte (non seulement des liens, mais aussi de la recherche, des indexs, etc), et de vraiment séparer le rendu du contenu.

On peut même imaginer faire de l'extraction et créer des bases de données sémantiques voire des bases de connaissances :D
Enfin, là, je m'enflamme ;)

Pour les personnes et ISBN je sais pas trop ce que tu veux dire

En gros, il y a des balises XML permettant de saisir ce genre d'information.
Dans le cas de l'ISBN ( International Standard Book Number ) (mais pas que) pour donner l'identifiant d'un ouvrage, on peut utiliser le balise biblioid.
Pour les personnes, la balise person permet de préciser l'adresse, le mail…

J'avais effectivement pensé aussi à Sphinx mais en y regardant de plus près après mon dernier commentaire, je me suis rendu compte que DocBook est beaucoup plus descriptif que les langages Sphinx, Markdown et consorts.
Je trouve ces derniers beaucoup plus bas niveau.

Sphinx décrit la structure en termes de titres, paragraphes et code source là où DocBook peut aussi décrire des entités comme les personnes, les adresses mails, les codes ISBN, les lignes de commande…

Au final, cela pas forcément d'importance sur le rendu mais cela peut permettre comme dit plus haut une meilleure gestion des recherches sur les documents qui portent à la fois de la forme et du sens.

Comme dit plus haut, ce n'est juste plus à la mode :)
Maintenant, c'est le Markdown et autres format simplifiés qui ont le vent en poupe.

Il s'agit du système utilisé par FreeBSD depuis plus de 15 ans pour toute sa documentation, avec, certes, un passage de SGML à XML (cf la documentation du contributeur).
De ce que j'ai pu voir, NetBSD l'utilise aussi.

Debian utilise DebianDoc dont le format ressemble étrangement à DocBook.

On ne peut pas dire que ce ne soit pas connu.

Personnellement, hormis quelques contributions FreeBSD, je l'ai aussi utilisé au boulot pour pondre une ou deux documentations techniques liées à l'administration système.
J'avais aussi réécrit l'intégralité des articles sur les failles de sécurité de Fred Raynal, Christophe Grenier et Christophe Blaess.

Je trouve que c'est pas mal mais il faut l'environnement pour la rédaction parce que sinon, c'est assez barbant.

A l'époque, j'utilisais le mode Emacs PSGML en raison de l'utilisation de SGML sur la documentation FreeBSD mais il semble exister un mode XML spécifique DocBook que je n'ai pas essayé.

Après, il semble qu'il y ait aussi des plugins pour d'autres éditeurs (cf. là)

J'ai l'impression qu'on navigue à la frontière entre le rôle du compilateur et celui de l'analyseur de statique de code.

Alors, je me suis aussi posé la question et j'ai fini par la poser au bon endroit à savoir sur le newsgroup.
Au final, c'est la norme qui définit la notion d'erreur de compilation et celle-ci ne parle que de validité du code source.
Bon, le compilateur, lui, le sait que ça ne va pas fonctionner mais c'est hors scope d'où le warning plutôt que l'erreur. Ceci dit, en utilisant l'option Warnings as errors à la compilation, ça revient au même ;)

Après, il y a les solutions type AdaControl pour l'analyse statique et Spark pour la preuve de code pour aller plus loin

c'est vérifié à la compilation

Petite correction, c'est effectivement juste un avertissement mais bon, les warnings en Ada, il vaut mieux les écouter ;)

Déjà, je me permets de renvoyer vers un excellent commentaire sur ton journal… Le mien :D

Je suis plus embêté par le concept de devoir fournir un cas par défaut pour un type comme tu le laisse supposer en commentaire

En fait, c'est normal que cela t'embête puisque c'est faux.
C'est la partie que j'avais laissée à l'appréciation du lecteur quand je parlais de mutabilité et qui se trouve décrite ici.
Lorsque l'on ne précise pas de discriminant par défaut, le type est immuable de facto, il faut définir le discriminant à la déclaration. Il devient alors impossible de changer de discriminant en cours de route et donc, il est impossible d'accéder à un composant qui n'est pas disponible et c'est vérifié à la compilation :)

J'aime bien ces dépêches-là, ça m'oblige à réfléchir comment je ferai ça dans mon langage préféré, qui est… L'Ada :)
J'ai donc tenté de faire les deux exemples.
Attention, il y a peut-être mieux :

with Ada.Text_Io; use Ada.Text_Io;

procedure Variant is

   type Formes is (CARRE, RECTANGLE);

   type Forme(De_Type : Formes) is 
      record
     case De_Type is
        when CARRE =>
          Cote : Positive;
        when RECTANGLE =>
           Longueur : Positive;
           Largeur : Positive;
     end case;
      end record;

   function Surface(La_Forme : Forme) return Positive is
   begin
      case La_Forme.De_Type is
     when CARRE =>
       return La_Forme.Cote ** 2;
     when RECTANGLE =>
        return La_Forme.Longueur * La_Forme.Largeur;
      end case;
   end Surface;

   Mon_Carre : Forme := Forme'(De_Type => CARRE, Cote => 2);
   Mon_Rectangle : Forme := Forme'(De_Type => Rectangle, Longueur => 5, Largeur => 2);
begin
   Put_Line("Surface " & Positive'Image(Surface(Mon_Carre)));
   Put_Line("Surface " & Positive'Image(Surface(Mon_Rectangle)));
end Variant;

L'avantage ici est que, comme en Haskell, il est impossible dans un CASE d'oublier une alternative, le compilateur ne voudra jamais.
De fait, l'ajout d'un élément à l'énumération va forcer le développeur à compléter son record et aussi à compléter la fonction Surface.
J'ai laissé de côté la notion de mutabilité des variants mais pour ceux que ça intéresse, c'est là :)

Pour le deuxième exemple, c'est plus facile, la programmation multi-processeurs fait partie de la norme et la version 2012 du langage a introduit l'annexe Multiprocessors (ça, c'est là)

with System.Multiprocessors; use System.Multiprocessors;
with Ada.Text_Io; use Ada.Text_Io;

procedure MT is
   type CPU_CONFS is (TOUS_LES_CPUS, LA_MOITIE_SEULEMENT, AUTRE_CHOSE);

   subtype NB_CPU is CPU range 1 .. Number_Of_CPUs;

   procedure SetGlobalThreadCount (Config : CPU_CONFS) is -- TOUS_LES_CPUS est comme CPU'Last
   begin
      -- Quelque chose ici avec des Task et autres joyeusetés
      -- en fontion de la conf

      case Config is
     when TOUS_LES_CPUS =>
        Put_Line ("Zou, à fond " & CPU'Image(Number_Of_CPUs));
     when LA_MOITIE_SEULEMENT =>
        Put_Line ("Mollo " & CPU'Image(Number_Of_CPUs / 2));
     when AUTRE_CHOSE =>
       Put_Line("Smart");
      end case;

   end SetGlobalThreadCount;

   procedure SetGlobalThreadCount (combien : NB_CPU) is
   begin
      -- Un autre truc en fonction du nombre de CPU
      Put_Line("nb CPU : " & NB_CPU'Image(combien));
   end SetGlobalThreadCount;

begin
   SetGlobalThreadCount(LA_MOITIE_SEULEMENT);
   SetGlobalThreadCount(12);
end MT;

Number_Of_CPUs étant une fonction dont la valeur n'est pas connue à la compilation, le compilateur ne détecte pas que 12 CPUs, c'est trop… Ça donne une jolie exception CONTRAINT_ERROR qu'il reste à gérer.

Voilà donc ma petite contribution et merci pour le petit exercice et cette petite présentation bien sympa d'exemples de typage statique en Haskell.

Vous auriez été déçu si j'avais réagi pour promouvoir ce langage :)
En Ada, il y a 3 attributs pour faire ça :
- S'Rounding qui renvoie l'entier le plus loin de zéro
- S'Unbiased_Rounding qui ramène au plus proche entier pair
- S'Machine_Rounding dont la norme précise que le retour est spécifique à la machine cible

Merci pour ce journal rafraichissant en tout cas

Les écoulements turbulents sont chaotiques

J'aurai envie de dire : "Les écoulements turbulents sont chaotiques, jusqu'à preuve du contraire…"
Mais, c'est parce que j'ai tendance à penser la science et sa progression comme telles :)

en tout cas peut-être qu'un fail2ban peut éviter ce genre de problème

On peut aussi utiliser les temps entre tentatives de connexion sur le firewall.
Petit exemple avec PacketFilter :

table <ssh-bruteforce> persist file "/etc/pf.table.fail2ban"
block in quick from <ssh-bruteforce>
pass in quick on $ext_if proto tcp from any to ($ext_if) port ssh flags S/SA keep state \
( max-src-conn 100, max-src-conn-rate 3/10, overload <ssh-bruteforce> flush global)

Ensuite, moi, je rajoute du One Time Password en plus :)

Question sans doute idiote mais pourquoi des hard links ? Perso, je ne me rappelle pas en avoir créé une seule fois en 20 ans :)
Dans quel cadre en utilises-tu ?

Généralement la fréquences des archives diminue avec l'age (quotidien sur la dernière semaine, hebdomadaire sur l'année, mensuel ensuite par exemple avec des durée de rétention limité) ce qui permet de gagner BEAUCOUP de place.

D'ailleurs, c'est le but même des outils comme Bacula.

Va falloir arrêter un peu avec ça ! A chaque fois que l'on parle d'Ada, on y a le droit.
Le langage n'y est pour rien quand il y a décision du développeur de lever les protections sur une variable pour raison de performances.

à Paris, non à Marnes La Vallée, non à Chessy … Bref c'est ce week end et c'est en région parisienne !

Ah ouais, c'eut été carrément l'horreur que ça se passe en "région" :D

Par moment, je me demande si Git n'a pas fonctionné en partie grâce au culte de la personnalité autour de Linus Torvalds.
Il y avait déjà de bons outils à l'époque mais, bien entendu, il n'y a pas de meilleur outil que celui que l'on fait soi-même… :)

Il n'existait pas déjà cvs ou svn à cette époque ?

Si mais surtout il y avait déjà Darcs et Monotone en outils de gestion de versions décentralisé Open Source

Non, au tout départ, c'est bien un problème d'exception matérielle dû à un dépassement de capacité (voir l'explication).
Mais au final, c'est un problème de design puisque la centrale inertielle n'était pas supposée fonctionner après le décollage et encore moins sur Ariane 5 :)
Du coup, on est d'accord, le code mort, c'est mal :D

Je me doutais que ça finirait par en parler. Et puis j'aime bien les news sur les nouveaux langages.
Dès qu'on parle de bug, on parle de l'emblématique bug d'Ariane 5 :)

Bon, je vais pas faire tout un laïus sur le fait que la norme d'Ada autorise l'utilisation d'un GC mais que je n'en ai pas encore vu :)
Globalement, on n'en a pas vraiment besoin vu comment tout ce qui est lié aux pointeurs et à l'allocation dynamique est contraint.
D'ailleurs, j'ai vu parler de pool de mémoire et c'est effectivement un mécanisme qui existe dans le standard.

C'est vrai que grâce à un langage sans GC Ariane 4 n'a jamais eu ce genre de problème, n'est-ce pas ?

En fait, c'est Ariane 5 (cf. Vol_501_d'Ariane_5). Et en plus, ça n'a rien à voir avec une histoire de fuite mémoire mais le problème vient d'un dépassement de capacité sur des variables non protégées.

La difficulté de la gestion manuelle de la mémoire dans une application complexe, par exemple, est un effet de système inévitable

Certes mais il y a encore beaucoup de projets très complexes qui utilisent une gestion manuelle de la mémoire sans que celle-ci soit forcément complexe en elle-même. Rien n'est inévitable… Après, je ne sais pas ce que tu appelles complexe.

un téléphone "intelligent" aujourd'hui est suffisamment puissant pour faire tourner une JVM entière

La fameuse JVM entière est, quant à elle, codée dans un langage n'utilisant pas de GC…
Comme quoi les deux approches ont leur intérêt.