Blackknight a écrit 1240 commentaires

Les débordements d'entiers bouclent en rust

Par contre, ce que je n'avais pas vu, c'est la différence de comportement entre le mode debug et le mode release

The current status in Rust was decided in RFC 560:
in debug mode, arithmetic (+, -, etc.) on signed and unsigned primitive integers is checked for overflow, panicking if it occurs, and,
in release mode, overflow is not checked and is specified to wrap as two’s complement.

Ca, je trouve ça piégeux.

sauf qu'en rust c'est un comportement défini).

En C11 aussi il s'agit d'un comportement défini, tant que l'on parle d'entiers non signés (cf. là).
Par contre, oui, pour les entiers signés, c'est un undefined behaviour.

Il y a aussi autre chose et non des moindre, c'est que si les spécifications ont toujours été assez libre d'accès les compilateurs ont toujours eu un train de retard et sont closed-sources pour les plus complet.

Vrai en 1983, beaucoup moins à partir de 1995… D'ailleurs Gnat existe depuis cette date, quand le compilateur a passé l'ACATS 95 avec succès.

En fait Ada est un langage qui ne proposait pas vraiment de solutions techniques. Et au départ, beaucoup de ses spécificités n'étaient pas implémenté fautes de solution techniques.

Est-ce au langage de fournir les solutions techniques ? Les standards C et C++ ne fournissent absolument de façon d'implémenter le compilateur. D'ailleurs, il y a quelques années, au boulot, pour des raisons de performances, on utilisait ICC (Intel C++ Compiler) en lieu et place de GCC, les deux compilateurs différent dans la génération du code assembleur.

Aujourd'hui c'est un peu différent car GNAT arrive a un niveau correct (mais derrière les version payantes, et même très chères).

Encore une fois, je veux bien une source.

Ceci lui fait un gros handicap marketing, il a une image de langage élitiste, mal fini et cher (un peu comme COBOL). Rust est tout au contraire, open-source, plein de librairies, avec un compilateur open-source…

Ce dont tu parles date d'il y a plus de 30 ans et il y a un compilateur opensource conforme à la norme depuis 27 ans.
Par contre, oui, il n'y a pas plein de bibliothèques contrairement à Rust.

Coder en Ada est bien plus long et complexe que coder en Rust.

C'est une question de point de vue :)

A savoir qu'on peut vérifier qu'un programme Ada ne fera pas une boucle infini ou ne fera pas une multiplication qui dépassera la valeur d'un Int. Mais pour arriver a ce résultat, il faut tout dire a Ada.

Alors si on parle de vérifier, ce sera via du Spark mais sinon, il y a juste à définir des types ce qui n'est pas en soi insurmontable.
Alors oui, il faut tout dire mais ça documente aussi beaucoup le code.

Surtout qu'Ada perd un peu en performance par rapport a Rust ou C/C++.

Source ? Usuellement, on estime que le code Ada est 30% plus lent que le code C et équivalent au code C++, sans retirer les runtime checks sinon, c'est équivalent au C. Mais bon, j'ai pas plus de source :D

Oui, bien sûr, il s'agit de Fabien Chouteau.
Il travaille chez Adacore et est très sympa :)

Je ne suis pas sûr de bien comprendre mais pour ton exemple de vitesse

with Ada.Text_Io; use Ada.Text_Io;

procedure Vitesse is
   type Distance is new Positive;
   type Speed is new Positive;

   function "*"(Left: Duration; Right: Distance) return Speed
   is
   begin
      return Speed(Left * Positive(Right));
   end "*";

   function "*"(Left: Distance; Right: Duration) return Speed is ("*"(Right, Left));

   My_Dist: Distance := 12;
   Time : Duration := 1.0;

begin
   Put_Line("Speed = " & Speed'Image(My_Dist * Time));
end Vitesse;

Les types Speed et Distance dérivent du type Positive, la multiplication entre deux distances et entre deux vitesses est donc définies.
Par contre, pour mélanger les types entre eux, je dois préciser de quoi il s'agit et comment doit être fait le calcul.
Le type Duration est quant à lui un type flottant.

Bon, j'ai dû le rêver :D
La seule info que j'ai trouvée approchant est celle de Fabien sur Reddit.

Certaines annexes sont toutefois normatives.

Aujourd'hui, il me semble que seule l'annexe Distributed Systems n'est pas implémentée dans Gnat mais bon, c'est PolyORB qui s'en charge en fournissant en plus un bus CORBA (cf. l'excellente présentation au FOSDEM 2019 :D)

Il faut distinguer deux choses:

• Spark est un sous-ensemble d'Ada et se compile donc normalement avec le compilateur Ada
• Un code Spark peut (et devrait sinon, autant faire de l'Ada, c'est plus simple) être vérifié

Les temps de compilation sont donc les temps du compilateur Ada qui n'est pas non plus franchement le plus rapide du Far West.
Ceci dit, c'est normal, il compile beaucoup plus de choses qu'un compilateur C, ne serait-ce que les spécifications (en gros, les headers C) et vérifie tout une batterie de règles de cohérence (compatibilité des types, portée des pointeurs…).

A cela, s'ajoute dans le cas de Spark, l'étape de preuve du programme.
Cette étape fait appel à un autre outil que le compilateur dont le but est de transcrire les éléments Spark (post-, pré-conditions, invariants de boucle, assertions) dans le langage Why3.
Le "programme" Why3 est ensuite envoyé au moteur de preuve pour être analysé. Cette étape peut être très longue, beaucoup plus qu'une simple compilation mais l'enjeu n'est vraiment pas le même qu'une "simple" compilation.

A ce jour, les "provers" CVC4, Z3 et Alt-Ergo sont supportés et il est parfois nécessaire de faire passer son programme à la moulinette d'un ou plusieurs de ces programmes.

Petit anecdote, après discussion avec Yannick Moy à l'OSXP , Adacore a commencé à décorer la bibliothèque standard avec du Spark, histoire de prouver qu'il n'y a pas d'erreur dedans… Il semblerait qu'ils aient d'ailleurs trouvé une petite erreur passée inaperçue depuis des lustres :D

Voilà, j'espère avoir répondu à la question sans avoir dit trop de conneries :D

Il semblerait que la version GNAT Community soit un peu plus en avance que la version GNAT FSF (en terme de version, d'après ce que j'ai pu lire).

Oui, les développements sont faits avant tout pour Gnat Pro ce qui est compréhensible vu que c'est le fond de commerce d'Adacore.
Ensuite, tous est remis dans la version Community avant d'être finalement mergé dans la version FSF.

De mémoire, la version Community 2021 sera la dernière fournie par Adacore, il ne restera donc que la version FSF.

On verra donc ce qu'il se passera en 2022 :)

Après vérification sur mon exemplaire de la norme AFNOR d'Ada 83 et le site de Ada Information Clearinghouse, il se trouve que la norme est le manuel de référence.
Toutes les révision de la norme sont donc bien accessibles gratuitement ici.

Bizarre, y a tout plein de liens en bas de cette page-là dont le Reference Manual et le manuel utilisateur.

Après, il y a quelques entrées de blog chez Adacore qui sont intéressantes.
Il y a, par complexité croissante :

• Le passage d'Ada à Spark sur un objet simple, une pile
• la réimplémentation d'un code Rust en Spark qui colle bien au sujet du journal
• Une implémentation prouvée de TweetNaCl

En "libre" je ne connais que GNAT. Et encore, il me semble qu'il n'implémente pas tout Ada. Les seuls compilateurs à implémenter entièrement la norme sont propriétaires.

Je veux bien que tu dises quelles parties ne sont pas implémentées. En effet, Adacore, qui est le plus gros contributeur à Gnat, fait justement l'effort de coller à la norme de très près et est même en avance par rapport à la publication des révisions.

Peut-être parles-tu des annexes ?

En fait, c'est moi "j'ai oublié qui" :)
En même temps, on n'est pas très nombreux à parler d'Ada, le langage, ici :)

Je sens que ma question va avoir l'air conne mais y a que moi qui essaye de monter des VPN IKEv2/IPSec ?
Bon,ok, j'avoue que c'est moins trivial que OpenVPN.. :)

Perso, on avait regardé ça il y a quelques années à POSS avec Benoît mais de mémoire, c'était dans la base en direct.

Oui, bon, évidemment, ça va être dur de rivaliser :D

Et merci.

Je ne traîne pas sur le site depuis 1998 mais ça doit pas être loin.
De mémoire, mon id dans la base est assez petit d'ailleurs :)

on peut peut-être corréler ça avec l'activité informatique des industries qui utilisent ce langage (notamment aéronautique si j'ai bien compris) ?

Pour avoir bossé quelques années dans le secteur, je n'y ai vu que trois ou quatre projets en Ada. En même temps, c'est chiant, les trucs fonctionnent pendant des lustres, difficile de vendre de la maintenance :D

Du genre un gros développement qui pousse les gens à chercher des tutoriels pour l'ancien et le nouveau ?

Alors dans ce cas, on peut se trouver dans le cas de portage vers d'autres langages mais le bon indicateur, c'est le nombre d'offres d'emploi et de ce côté-là, c'est pas forcément le feu d'artifice.
Ceci dit, apprendre Ada est largement à la portée du développeur C/C++ ou Java donc au final, c'est pas bien compliqué de recycler un dev… Mais ça, je ne crois pas que grand monde le fasse.

Oui, c'est tout à fait possible mais on peut aussi rêver quand on voit arriver quelques nouveaux sur StackOverflow.

Oui, comme vous l'avez dit Ysabeau et toi, j'ai bien pensé au Youtube qui pose problème.
D'ailleurs, moi aussi, ça me démange d'où la chaîne Ada sur Peertube.
D'un autre côté, je préfère que les 8h heures de vidéo restent sur Youtube, mon quota sur Peertube.social est pas assez important pour accueillir une telle vidéo :D

Merci pour le +1 ;)

Tiens, ça, je ne m'attendais pas à me faire moinser pour un partage de lien sur de l'info :)
J'aimerai bien savoir pourquoi

En entreprise, on voit beaucoup plus de Java et de Go que du Python et du Rust.

Ca dépend, dans ma boite, c'est Java, C#, PHP et du Python surtout côté data science .
On a un seul projet en Go mais parce que c'est un ajout de fonctionnalités à Mattermost et effectivement, pas de Rust.

T'es la plus forte :)

Bon, j'ai eu le clic trop facile… Encore
C'est de l'anglais !!

Y aurait de nos chers modos qui pourrait me changer ça siouplait ?