AdaCore Tech Day 2019

Merci pour cet article intéressant.

Au risque de poser une question qui fache, quels sont les avantages de Ada par rapport aux autres langages ? Sans être spécialiste du domaine de programmation sûr (sans quoi je ne poserai pas la question), je sais qu’il existe un compilateur d’un sous-ensemble du C qui peut valider un code, des trucs de preuves de validité du genre Coq, ou des langages qui visent une grande sécurité (Rust).

Qu’est-ce qui rend Ada particulier aujourd’hui ? Je vois peut-être un compromis entre l’utilisabilité et son caractère éprouvé.

Sinon, d’un point de vue non professionnel (opensource, amateur…), Ada est-il utilisé ? Typiquement, je ne connais pas de logiciel libre de bureau en Ada, mais peut-être me trompè-je.

L’avantage le plus marquant est qu’Ada formalise la programmation par contrat (pour chaque procédure ou fonction, on peut préciser dans l’interface des modules : préconditions, postconditions, variants, invariants…).

C’est donc un confort incomparable quand on fait de la programmation modulaire, et en particulier quand il s’agit de relire ou de maintenir des applications (la syntaxe est très lisible). Cela va donc plus loin que les preuves de programme type Coq (pour ce que je m’en souviens), et représente une garantie de fiabilité

Déjà, la norme Ada sort avant les mise-à-jours des compilateurs, de plus ils refusent tout sur et sous-ensemble, ce qui évite de se retrouver avec des incompatibilités d’un compilateur à l’autre.

Tu parle de Frama-C ?

Frama-C est une bibliothèque qui permet de faire de la preuve formel en C. En Ada, tu a directement Spark, un sous-ensemble du langage qui permet de faire de la preuve formel, sans rien rajouter au langage.

Demande à @Ksass`Peuk (un dev de Frama-C) de qui entre code C et un code Ada/Spark est le plus facile à prouver.

Là je ne vais pas trop m’avancer car je n’ai pas appris Rust (ou Go, ou le nouveau langage à la mode ^^), mais ce genre de langage n’apporte généralement rien de nouveau, ou simplement une ou peu de nouvelles idées. Rust par exemple apporte le système d’ownership, ce qui semble très intéressant (je n’ai pas regardé en détail), d’ailleurs, un des types d’ownership a été ajouté à Spark pour faire de la preuve formel avec un peu de pointeurs.

Le truc, c’est que je pense que les gens trouvent plus facile de créer un nouveau langage que de chercher avec les bons mots-clefs sur leur moteur de recherche favori pour voir s’il n’existe pas un langage qui répond déjà aux besoins.

Dire que rust (attention, je ne parle pas de toi : P) est un langage révolutionnaire en permettant de faire des programmes sûrs, je suis désolé, mais ça existe au moins de puis 1983 (première parution d’Ada), voir peut-être même avant.

Aujourd’hui on se retrouve noyé dans un choix toujours grandissant de langage. Je pense que si on a une bonne idée sur un concept qui n’est pas encore implanté dans un langage, plutôt que de créer un nouveau langage, il faudrait mieux essayer de l’intégrer à un langage déjà existant. Par exemple en Ada 2005, ils ont rajouté les interfaces, tout droit emprunter de java.

Là forcément mon avis risque d’être un peu biaisé car c’est un langage que j’adore.

Déjà, un truc que je trouve super avec Ada, c’est que tu peux créer tes propres types scalaires.

Par exemple, si tu travailles avec les ports d’une machine, tu peux créer un type d’entier allant uniquement sur la plage de définition des valeurs des ports :

-- Définition du type
type Port_T is range 0 .. 65_535;

-- plus loins

Default_Port : constant Port_T := Port_T'Last; -- utilise la dernière valeurs de la plage du type Port_T

Tu noteras également l’underscore (complètement optionnel) pour séparer des paquets de valeurs (milliers, etc.). C’est tout con et ça permet de gagner en lisibilité. À ma connaissance, c’est le seul langage qui propose cela.

Comme l’a mentionné @MichelPro, tu as également la programmation par contrat.

Un exemple tout bête : imaginons que tu as une fonction qui retourne la somme de deux entiers positifs, tu peux mettre un contrat sur la fonction pour vérifier par exemple que les paramètres d’entrée sont supérieurs à 0 (c’est pour l’exemple, car il existe un type Positive) et que le résultat est bien la somme des deux valeurs (encore une fois, c’est un exemple) :

function Sum (A, B : Integer) return Integer
   with
   Pre  => A > 0 and B > 0,
   Post => Sum'Result = A + B;

Un autre truc que j’adore également, c’est le multi-tasking. Encore une fois, c’est intégré au langage, tu peux créer tes propres types de tâches ou d’objets protégés.

Exemple d’un simple sémaphore :

-- Spec
protected type Semaphore (K : Positive) is
   entry P;
   procedure V;
private
   Count : Natural := K;
end Semaphore;

-- Body
protected body Semaphore is
   entry P when Count > 0 is
   begin
      Count := Count - 1;
   end P;
   procedure V is
   begin
      Count := Count + 1;
   end V;
end Semaphore;

Exemple utilisant objet protégé et tâche, le dîner de philosophes (source) :

with Ada.Numerics.Float_Random;  use Ada.Numerics.Float_Random;
with Ada.Text_IO;                use Ada.Text_IO;
 
procedure Test_Dining_Philosophers is
   type Philosopher is (Aristotle, Kant, Spinoza, Marx, Russel);

   -- Spec
   protected type Fork is
      entry Grab;
      procedure Put_Down;
   private
      Seized : Boolean := False;
   end Fork;

   -- Body
   protected body Fork is
      entry Grab when not Seized is
      begin
         Seized := True;
      end Grab;
      procedure Put_Down is
      begin
         Seized := False;
      end Put_Down;
   end Fork;
 
   Life_Span : constant := 20;    -- In his life a philosopher eats 20 times
 
   task type Person (ID : Philosopher; First, Second : not null access Fork);
   task body Person is
      Dice : Generator;
   begin
      Reset (Dice);
      for Life_Cycle in 1..Life_Span loop
         Put_Line (Philosopher'Image (ID) & " is thinking");
         delay Duration (Random (Dice) * 0.100);
         Put_Line (Philosopher'Image (ID) & " is hungry");
         First.Grab;
         Second.Grab;
         Put_Line (Philosopher'Image (ID) & " is eating");
         delay Duration (Random (Dice) * 0.100);
         Second.Put_Down;
         First.Put_Down;
      end loop;
      Put_Line (Philosopher'Image (ID) & " is leaving");
   end Person;
 
   Forks : array (1..5) of aliased Fork; -- Forks for hungry philosophers
                                         -- Start philosophers
   Ph_1 : Person (Aristotle, Forks (1)'Access, Forks (2)'Access);
   Ph_2 : Person (Kant,      Forks (2)'Access, Forks (3)'Access);
   Ph_3 : Person (Spinoza,   Forks (3)'Access, Forks (4)'Access);
   Ph_4 : Person (Marx,      Forks (4)'Access, Forks (5)'Access);
   Ph_5 : Person (Russel,    Forks (1)'Access, Forks (5)'Access);
begin
   null; -- Nothing to do in the main task, just sit and behold
end Test_Dining_Philosophers;

Et je ne te parle même pas de l'annexe distribué.

Il y a quand même une petite ironie sur Ada. Quand ils l’ont sortie, ils se sont dit « C’est le langage du turfu », le truc, c’est que c’était plus destiné à l’armée et SURTOUT, les compilo étaient hors de prix (donc bye bye les universités). Durant la même période tu as C qui est sortie avec son système (UNIX) et son compilo, du coup, qu’est-ce qu’on fait les gens ? Ils ont choisi C. Ce qui a amener à délaisser Ada (sans oublier qu’a l’époque, il était un peu en avance sur leurs temps sur certains concepts que les dev de l’époque ne comprennaient pas). Les mainteneurs d’Ada on changé leurs fusils d’épaule à la mise à jour suivant en fournissant un interfacage C, COBOL et FORTRAN de mémoire. Du coup tu peux appeler du code C ou C++ depuis Ada et inversement.

Et oué, là il y a un problème. Ada est pas très utilisé en open source; tu peux trouver des petites lib ou jeux faites à Ada (Ada-zip, etc.) mais pas de libreoffice version Ada. Et c’est là que tu te rends compte que les sites qui te dises quels sont le langage le plus utilisé, le plus à la mode où je sais pas quoi sont généralement tous biaisés, car il se base sur des données généralement publiques (open-source). Ada est très utilisé dans l’industrie et principalement dans les systèmes critiques, mais tu ne vas pas trouver le code d’Arian 6 (fait en Ada 2012), le code d’un guidage de missile ou d’un CBTC sur Git Hub. Et généralement, les entreprises qui en font ne le crient pas par sur tous les toits.

Enfin voilà, tout cela mériterait un billet consacré, mais pour que je m’y mettent, il faut que je réunisse le facteur temps + motivation.

Merci pour cette réponse très complète. La programmation sûr m’intéressant dans l’idée depuis un moment, aurais-tu un bon tuto à recommander sur Ada ?

Alors,

En français, tu as le cours d’Ada qui est sur le site (portage du site du zero). Il contient quelques fautes et le chapitre consacré à GTK est en partie obsolète. Il donne déjà un point de départ sur Ada.

Sinon, comme je l’ai mentionné dans le billet, AdaCore on développé un site permettant d’aprendre Ada (et Spark).

AdaCore propose également des livres disponnible gratuit sur Ada, Spark et même sur certaines certifications dans le ferroviaire et l’avionic.

Niveau livres, tu as la référence dans le domaine, le Barnes (Programming in Ada 2012).

Et pour plus de preuve formel, avec Spark cette fois si, tu as Building High Integrity Applications with SPARK qui est également une référence dans le domaine Spark (je dois le lire, ou à minima le survolé pour ma thèse d’ailleur ^^).

La communauté Ada, comparé aux communautés d’autres langages du genre C, C++ ou Java est relativement petite, mais tu es entouré de personnes très très compétentes avec chacun son domaine de prédilection. On n’échange pas mal sur (le préhistorique) comp.lang.ada et fr.comp.lang ada ou sur stackoverflow.

Il y a beaucoup à dire ici. Notamment, il existe deux outils "complètement formels", si l’on peut dire, pour le langage C. CompCert, un compilateur certifié, et Verasco un analyseur vérifié. CompCert ne valide pas le code. Il garantit que si un programme C ne contient aucun undefined behavior (ce qu’il ne vérifie pas), alors le code produit en sortie correspond sémantiquement au programme C que l’on a écrit (et optimise).

Verasco est un interpréteur abstrait basé sur CompCert. Il permet de montrer l’absence d’undefined behaviors, MAIS c’est dur, donc il est plutôt commun qu’il réponde "je ne sais pas".

C’est pour ça qu’on fait aussi des analyseurs qui sont formels mais pas complètement (au sens : l’analyseur n’est pas prouvé correct) comme Frama-C parce que l’on est généralement capable de faire des algos plus tricky dont on a de bonnes raisons de penser qu’ils sont bons mais qui seraient potentiellement très difficiles (et donc très couteux) à prouver formellement.

Nope. Même si Ada est un langage plutôt bien foutu, il ne donnait (et ne donne toujours) pas de safety by design. Il est très facile de faire un truc tout pété en utilisant des fonctionnalités aussi stupides que le new qui est fourni en Ada, ou alors en attaquant des programmes concurrents. En Rust, pour péter les garanties données par le système de types, il faut utiliser des blocs unsafe.

Rust a très clairement apporté quelque chose de neuf. Un système de types utilisable en production qui donne des garanties de memory safety, y compris dans un contexte concurrent. Il y a eu des langages jouets capables d’arriver à faire quelque chose de ce genre, mais certainement pas de langages utilisés en production et avec les performances qu’offre Rust.

EDIT :

Sans faire la vérification des dits-contrats, ça n’apporte pas vraiment de fiabilité.

Un truc qui est chiant avec Ada, c’est la lourdeur des types sommes/algébriques et l’absence de construction de filtrage de motif satisfaisante. On peut faire des variant records, qui offrent plus de sûreté qu’une union de C, mais cela impose le même style de programation assez lourd où on teste un tag, on accède aux champs, etc.; pour définir des structures d’arbre syntaxique par exemple, c’est très lourd. À quand l’ajout de filtrage de motif digne de ce nom ?

Une chose qui me met un peu mal à l’aise dans ce billet, c’est l’aspect publicitaire pour une société privée. AdaCore est une boîte qui fait plein de choses très bien et qui porte de belles valeurs en terme de programmation, mais il n’empêche que le billet, par la façon dont il est rédigé, ressemble plus à du contenu écrit par un influenceur sponsorisé qu’à un résumé d’un événement technique. (Un peu comme le serait un retour d’expérience sur la conférence Apple ou Microsoft de l’année.)

Est-ce que, au moins, quand on écrit ce genre de billets sur ce site, on pourrait s’imposer la discipline de clarifier les liens qu’on a avec la structure que l’on décrit ? (Est-ce que l’auteur est employé d’AdaCore, ou alors membre d’une structure qui travaille avec AdaCore ?) Je lis pas mal de nouvelles sur Linux Weekly News, où les auteurs précisent par exemple quand les frais pour assister à un événement ont été couverts par une structure privée. Je ne demande pas que les auteurs de billets sur ZdS s’auto-astreignent au respect des principes journalistiques les plus stricts, mais je pense qu’il serait bon que les partis pris soient pleinement assumés et explicités, au moins au sujet des intérêts privés. (Vous vous souvenez du jour où le Site du Zero s’est mis à se lancer dans des jeux-concours pour gagner des cartes NVIDIA ?)

Je n’ai pas compris… Tu veux dire quoi par filtrage de motif ?

En même temps… c’est un évènement organisé par la société AdaCore. J’ai trouvé pertinent de parler de la journée étant donnée qu’elle (l’entreprise AdaCore) est un peu le leader dans le domaine de la compilation pour le langage de programmation Ada.

Ce n’est pas con ça. Je vais modifier le billet pour le mentionner. Juste pour le dire avant modif: je commence un doctorat (CIFRE) qui grosso modo touche à de la compilation, de l’analyse de code, structure de données, avec pour principale objective Ada (même si ce doit être plus langage agnostique possible). Je ne travaille pas pour/chez AdaCore. En revanche, j’utilise leurs compilo étant donnée qu’ils sont les seuls à fournir un compilo à jour. Je n’ai donc aucun lien directe avec eux, je ne possède pas d’action chez eux, et je ne suis pas sponsorisé/affilié/^(?:\w+é)$.