4 points par GN⁺ 12 일 전 | Aucun commentaire pour le moment. | Partager sur WhatsApp
  • Née dans le chaos logiciel du département de la Défense américain dans les années 1970, Ada est un langage dont les principes centraux sont le typage statique fort et la séparation entre spécification et implémentation
  • Grâce à sa structure en packages et à l’opacité de représentation, elle met en œuvre une encapsulation complète et a ensuite influencé les systèmes de modules de langages modernes comme Java, C# et Go
  • Les types à contraintes sémantiques, les génériques, la concurrence (task) et la conception par contrat sont autant de concepts qu’Ada a proposés avec plusieurs décennies d’avance, avant d’être repris par Haskell, Rust ou Swift
  • SPARK Ada élimine même les courses de données et les erreurs logiques par vérification formelle, et est utilisé dans des domaines à haute fiabilité comme l’aéronautique, le ferroviaire et les systèmes de défense
  • Ada n’est pas un langage populaire, mais il reste un « langage qui fonctionne correctement en silence », ayant posé les principes fondamentaux de la conception des langages de programmation modernes

Contexte de naissance d’Ada et philosophie de conception

  • Au début des années 1970, le département de la Défense des États-Unis (DoD) étudie une situation où plus de 450 langages et dialectes coexistent dans les systèmes d’armement, de logistique et de communication
    • Chaque système souffre de problèmes d’interopérabilité, de maintenance impossible ou de disparition de l’auteur initial
    • Cela provoque une crise des achats logiciels
  • Le DoD n’adopte pas un langage existant (COBOL, Fortran, PL/1, etc.) et passe par un processus de définition des exigences sur cinq ans
    • Strawman → Woodenman → Tinman → Ironman → Steelman
    • Steelman (1978) exige une séparation explicite des interfaces, un typage statique fort, une concurrence intégrée, une gestion cohérente des exceptions, l’indépendance vis-à-vis de la machine, la lisibilité et la vérifiabilité
  • En 1979, lors de la compétition entre quatre équipes (Green, Red, Blue, Yellow), l’équipe Green dirigée par Jean Ichbiah est retenue, et le langage reçoit le nom de Ada
    • Ce nom rend hommage à Ada Lovelace et symbolise l’intention du langage

Structure en packages et encapsulation

  • La structure centrale d’Ada est le package, avec une séparation physique entre la spécification (specification) et le corps (body)
    • La spécification est le contrat exposé à l’extérieur, le corps est l’implémentation, et le compilateur impose la relation entre les deux
    • Le code client ne peut pas accéder aux éléments absents de la spécification
  • Cette structure constitue un prototype de système de modules, que des langages ultérieurs n’ont imité que partiellement
    • Java, Python, JavaScript, C, Go et Rust ne mettent pas tous en œuvre la séparation structurelle complète d’Ada
  • Les types private n’exposent que leur nom, tandis que leur représentation interne reste totalement opaque
    • Le client ne peut pas connaître la structure interne du type et ne peut utiliser que les opérations autorisées
    • C’est une opacité de représentation plus forte que le contrôle d’accès private de Java
  • Java et C# ont évolué progressivement pendant des décennies vers un niveau d’encapsulation proche de celui d’Ada

Système de types et contraintes sémantiques

  • Ada définit mathématiquement la distinction entre type et sous-type
    • Exemple : type Age is range 0 .. 150 crée un type distinct doté d’une contrainte d’intervalle
    • Le passage entre types incompatibles est détecté comme erreur à la compilation
  • En 1983, le système de types d’Ada était bien plus expressif que ceux de C, Fortran ou Pascal
    • Les types à contraintes sémantiques permettent d’éviter des erreurs métier
  • Le record discriminé (discriminated record) est une structure qui possède des champs différents selon la valeur
    • Cela correspond aux sum types modernes ou aux types de données algébriques (ADT)
    • Haskell, Rust, Swift, Kotlin et TypeScript ont introduit le même concept plusieurs décennies plus tard

Génériques et polymorphisme

  • Les génériques d’Ada sont des unités pouvant prendre comme paramètres des types, des valeurs, des sous-programmes et des packages
    • Ils implémentent un polymorphisme statique (parametric polymorphism) avec vérification des types à la compilation
  • C++ (1990), Java (2004), C# (2005) et Go (2022), entre autres, n’ont introduit des fonctions similaires que plusieurs décennies après Ada
    • Java, avec le type erasure, perd l’information de type à l’exécution
    • Ada conserve les types à l’exécution et prend même en charge la paramétrisation de packages
  • Les génériques d’Ada offrent une expressivité proche du polymorphisme d’ordre supérieur (higher-kinded polymorphism)
    • Un concept comparable aux type classes de Haskell, aux traits de Rust et aux concepts de C++20

Modèle de concurrence et sûreté

  • Ada intègre dès 1983 la concurrence au niveau du langage avec les task
    • La déclaration de task et le modèle de communication par rendezvous mettent en œuvre une transmission de messages sans état partagé
    • Les channels de Go relèvent de la même famille de concepts CSP (Communicating Sequential Processes)
  • Ada 95 introduit les protected objects
    • Ils protègent l’accès aux données, avec une distinction entre procedure, function et entry
    • Ils fournissent des conditions de garde automatiques et une synchronisation sans verrou
  • SPARK Ada démontre formellement l’absence de courses de données, d’exceptions, d’erreurs de plage et de violations de préconditions ou de postconditions
    • Alors que le borrow checker de Rust ne garantit que la sûreté mémoire, SPARK va jusqu’à prouver la cohérence logique

Conception par contrat et sûreté vis-à-vis de null

  • Ada 2012 intègre les contrats directement dans le langage
    • Il permet d’exprimer des préconditions, des postconditions et des invariants de type
    • La chaîne d’outils SPARK les exploite pour la preuve statique
  • Il formalise au niveau du langage le concept de Design by Contract d’Eiffel (1986)
    • C++, Java, Python et Rust n’en proposent que des implémentations partielles ou limitées à des bibliothèques
  • Ada 2005 introduit les types not null afin de prendre en charge l’exclusion de null à la compilation
    • Par défaut, l’échec reste sûr via une exception à l’exécution (Constraint_Error)
    • Une approche comparable aux références nullable de C# 8.0

Structure de gestion des exceptions

  • Ada 83 introduit pour la première fois la gestion structurée des exceptions (structured exception handling)
    • Les exceptions sont déclarées avant utilisation, traitées selon leur portée, avec des règles de propagation explicites
  • Les checked exceptions de Java constituent une forme plus avancée, où l’appelant doit déclarer les exceptions
    • Ada autorise librement la propagation des exceptions
  • Rust supprime les exceptions et adopte une gestion des erreurs fondée sur le type Result
    • La contribution d’Ada est d’avoir rendu la propagation des exceptions structurée et prévisible

Annexes et structure de normalisation

  • La norme Ada comporte une structure d’extensions optionnelles appelée Annex
    • Les annexes C à H définissent des fonctionnalités par domaine : système, temps réel, distribué, calcul numérique, haute fiabilité
    • Les compilateurs doivent obtenir une certification indépendante pour chaque annexe
  • La conformité à la norme est vérifiée par les tests ACATS de l’ACAA
    • La structure normalisée d’Ada peut être utilisée directement pour la certification logicielle aéronautique DO-178C
    • C et C++ peuvent eux aussi être certifiés, mais Ada y est structurellement mieux adapté

Influence d’Ada et décalage de perception

  • Ada, en tant que langage porté par les pouvoirs publics, n’a pas retenu l’attention de la culture Silicon Valley
    • Il contraste avec une culture préférant des syntaxes concises issues de C
  • Les réussites d’Ada (aéronautique, ferroviaire, systèmes de défense) ont une faible visibilité précisément parce qu’elles n’échouent pas
    • Un système très fiable ne génère ni polémiques ni incidents
  • L’évolution des langages modernes converge vers des principes qu’Ada avait déjà formulés
    • Séparation spécification-implémentation, vérification statique des types, concurrence au niveau du langage, sûreté fondée sur le contrat, etc.
  • Ada est toujours utilisé dans des systèmes à haute fiabilité comme les avions, les chemins de fer ou les engins spatiaux, et demeure un « langage qui fonctionne correctement en silence »

Aucun commentaire pour le moment.

Aucun commentaire pour le moment.