Blackknight a écrit 1237 commentaires

Tu crois que cela ressemble à quoi des vrai spec ?

Ché pas, j'en ai jamais vu :)

Je faisais un référence un peu trop subtile à un défaut d'un cruise control de toyota qui s'est fait démonté par un expert aéronautique pour un procès : il ne se désactivait pas si la pédale de frein était enfoncé…

Houla, on parle de gens qui ont utilisé un OS spécialisé dans une version non certifiée en violant une tétra-chiée de règles du MISRA-C :D
En plus, le partitionnement de l'applicatif était foireux et j'en passe et des meilleures.

Au passage, si la NASA a bien fait une première étude, l'expert, Michael Barr, n'est pas issu de l'aéronautique.

Allez, pour le plaisir, le rapport

Concernant le code du drone, on dirait qu'il a seulement fait attention au overflow de calcul. Il faut que je relise moins en diagonal, je n'ai pas vu de propriété spécifiquement vérifier (genre l’arrêt d'urgence fonctionne dans tous les cas).

Du souvenir que j'en ai, c'est exact. Ceci dit, je n'ai pas lu l'intégralité du code mis à jour depuis.
Après, l'arrêt d'urgence fonctionne dans tous les cas reste assez vague comme contrat. On peut juste dire qu'il ne fera pas d'exception à l'exécution.

http://blog.adacore.com/how-to-prevent-drone-crashes-using-spark regardes le 2ième commentaires qui signale tout un tas de problème dans les specs du truc.

Certes mais ce sont des remarques sur ce que le stagiaire a implémenté pas une critique de la techno en elle-même.
Il ne faut pas se voiler la face quand même, il est peut être compliqué d'écrire les contrats de façon à ce qu'ils puissent être prouvés

Quand tu parles des preuves ici, tu parles Coq, Why3 ou Spark ?

Pour le dernier, je peux te donner cet exemple que j'avais déjà mentionné il y a longtemps dans un journal et qui montre que ce n'est pas toujours si matheux.
Le github n'a pas bougé depuis un an maintenant mais ça reste du Spark2014 donc c'est toujours valide.

Le problème est que le contrat est runtime et nécessite un test pour s’exercer. Il n'est pas possible d'avoir des contrats compile-time ou de vérifier leur cohérence entre eux ?

Il y a le même problème en Ada 2012 où les contrats sont effectivement là pour générer des assertions (cf. le wikibook) et donc seulement à l'exécution. Heureusement, cela est débrayable lors de la livraison au moyen d'une pragma.
Par contre, ces mêmes contrats sont la base de la programmation en Spark (pas le truc Apache, hein !) et sont, dans ce cas, traduits en langage intermédiaire, le Why3 (avec du Ocaml dedans), pour être ensuite passés aux moteurs de preuves

Mais la triste réalité du terrain, c'est que y'a une part non négligeable de ceux qui produisent n'utilisent les nouveautés technologiques que contraints par le projet.

Il y a un problème avec l'inverse, c'est quand un développeur utilise dans son coin, hors préconisation du projet, son petit bijou technologique bien hype que lui seul connait.
A partir de ce moment, c'est la mort pour la maintenance du projet si le mec se barre.
C'est du boulot pas de l'expérimentation.
D'ailleurs, quand on voit la durée de vie de certains frameworks JS, c'est pas franchement raisonnable de parier sur le tout nouveau tout beau.

Entièrement d'accord, mais si ton object fait 100ko, tu ne peux pas le copier.

Ben, justement, un const &var, ça ne copie que l'adresse pas l'objet et cela empêche la modification mais c'est vrai que le programmeur C++, surtout s'il vient du C, il aime pas ses trucs-là :D

Le plus simple, c'est d'avoir des objets immuables.

Oui ou modifiables seulement au travers de méthodes et pas en fournissant un accès direct.

Ocaml fonctionne comme ça. Si il y a plein de string partout, cela va bien plus vite, par contre, si il y a plein de string à vie courte, la consommation mémoire s'envole, car il est impossible de réutiliser un buffer.

Java fait idem pour les String ce qui entraine des petites incompréhensions chez certains quand ils modifient une chaîne passée en paramètres d'une méthode en espérant la voir mise à jour dans l'appelant :)

Justement, tout l'intérêt de Rust est de pouvoir faire du code MultiThreadé sans risque de problèmes de concurrences.

C'est bien pour ça que j'avais précis Hormis dans un contexte multithreadé.
J'ai effectivement bien vu l'intérêt, surtout par rapport au C++, qui reste somme toute très bas niveau pour tout ça.

C'est clair que c'est contraignant, mais les bugs de concurrences sont aussi hyper compliqués à résoudre, car ils dépendent énormément du contexte d'exécution. Ici, Rust fournit un langage plus difficile à appréhender (car il force le développeur à utiliser de nouveaux paradigmes), mais il fournit des concepts qui empêchent l'apparition de ces bugs

C'est clair que ce sont les bugs les plus difficiles à dénicher et que Rust fournit un moyen de minimiser les risques mais je trouve quand même la mécanique super lourde.

Si justement, Rust te garanti d'avoir un seul propriétaire de la mémoire, tu ne peux pas avoir 2 pointeurs qui se baladent, c'est plus facile à suivre

C'est pour ça qu'il vaut toujours mieux bosser avec des références const ou non en fonction des besoins et ne pas utiliser le passage de pointeur du tout.
Et là, finalement en C++, se trainer des const &var, ça devient presque aussi chiant que le Rust :)
Tout ça, c'est une histoire d'encapsulation et de gestion des responsabilités.
Quand on passe un pointeur, on abandonne la responsabilité du pointé à quelqu'un d'autre.
De toutes façons, les pointeurs, c'est sale :D

Au début seulement, si le code ne devient pas gros

Heu, c'est quoi la limite d'après toi ?

si personne n'a corrigé de bug avec un emplâtre mal placé

Ça, de toutes façons, même Rust n'y pourra pas grand chose.

car il peut devenir très compliquer de savoir quel traitement à déjà eu lieu et l'état réel du buffer.

Peux-tu donner un exemple plus clair?
Hormis dans un contexte multithreadé où l'accès à une même zone mémoire peut poser des problèmes, j'ai du mal à comprendre comment on peut ne pas savoir ce qui a été effectué sur une variable, y compris sa libération, l'exécution étant linéaire et les durées de vie connues (quoi appartient à qui notamment).

Rust fournit des contraintes où le programmeur se demande comment il va les contourner pour réussir à faire ce qu'il veut.

En Ada, si tu penses C/C++, tu en arrives à essayer de contourner le système de type, à tout faire via des access types.
Je pense que là, c'est pareil, ®om a commencé en Java où tout est référence (grosso hein, me taper pas dessus pour ça, j'ai pas envie d'écrire un commentaire de 60 lignes) et du coup, il faut faire de la gymnastique intellectuelle pour essayer de reproduire des patterns Java à Rust.

Je suis obligé de plussoyer :D
Mais je m'étais juré de ne pas en parler !!

Le problème, c'est que ça va m'obliger à parler des types Access et là, je suis pas super bon, je n'en ai quasiment jamais utilisé, les modes de passage de paramètres suffisant dans la plupart des cas ;)

C'est vrai que les borrowing rules sont assez contraignantes pour la conception d'une application.

Ça s'apparente même à de la contorsion plus qu'à de la programmation par moments.
Il faut avouer que ce genre d'écritures

Rc<RefCell<Storage>>

C'est quand même pas super raisonnable pour coder un patron de conception des années 80 :D

Attention, je ne dis pas que je ne comprends le pourquoi de cette écriture mais cela montre bien que le système d'emprunts est une grosse usine à gaz et me fait plus penser à une rustine d'une façon de faire issue du C++.
En même temps, Graydon Hoare est issu du monde C++ (cf. Monotone) donc ce n'est pas plus étonnant que ça.

A la vue des derniers commits de Linus, il s'agit majoritairement de ré-intégration de branches ou de tags.
Ceux-ci ont déjà été retravaillés et mergés en amont donc pour cette tâche d'assez haut-niveau, pas besoin de ré-écrire Git.

France Insoumise a été choisi par 5% du peuple aux élections législatives (quelle représentativité!)

Ttttt, 5% des suffrages exprimés. C'est pas pareil quand le taux d'abstention est de 56%, c'est pire :)
Ceci dit, ça vaut aussi pour les autres.

C'est la dure vie du commentateur de LinuxFr mais compte tenu des notes à ses derniers commentaires, cela devrait changer assez vite :)

Est-ce que l'algo seul peut être prouvé sans que le programme complet soit prouvé ? Je ne sais pas.

Alors, tout dépend de la techno utilisée.
De ma petite expérience en Spark, on peut prouver des morceaux du programme en ne marquant que certaines unités de compilation comme étant en Spark.
Typiquement, les entrées/sorties sont exclues du sous-ensemble vérifiable par Spark.
Mais, il faut bien voir qu'il faut quand même écrire les annotations Spark dans le code Ada pour pouvoir prouver quoique ce soit et ça, c'est pas forcément toujours très aisé.

Côté Rust il y a quelqu'un qui travaille dessus

Après, j'ai aussi vu un Coq2Rust permettant donc de créer son programme Rust à partir d'un programme Coq mais j'avoue ne pas avoir regardé plus que ça.

…qui fournit les théorèmes, des preuves et la complexité algorithmique du programme

Alors :

• théorèmes, ok (cf. commentaire de Kantien, c'est basé sur la théorie des graphes.
• Complexité algorithmique du programme : ok
• Preuves : Pas ok

De quoi parle-t-on au juste ici pour les preuves ? Démonstration mathématique basée sur les théorèmes précédant ou preuves de bon fonctionnement du programme ?
Il ne semble pas qu'il y ait, en Rust, moyen de prouver le bon fonctionnement du programme.
Si ?

Or, de mon expérience de cycliste urbain, le danger vient des bagnoles

Heu, oui mais il y a aussi du non-respect des feux, des stops et, pour moi qui suis piéton (et cycliste aussi), du non-respect des passages cloutés.
Pers, quand je suis à vélo, c'est gilet jaune, casque et bandes jaunes qui, au passage, tiennent aussi le bas du pantalon.
Alors forcément quand je suis à pied et que j'évite de justesse un vélo qui a décidé que le feu rouge le ralentissait et qui déboule de derrière un camion, ça m'énerve. Bien sûr, je passe sur l'absence de casque et de tout moyen permettant d'augmenter la visibilité du dit-cycliste.
Bien sûr, ça pourrait être un cas isolé mais quand une collègue vous dit que dans bien des cas, appliquer le code de la route à la lettre est dangereux pour les cyclistes…

Finalement, il y a bien une hiérarchie sur les routes : camion -> voiture -> moto -> vélo -> piéton.

J'ai l’impression que vous ne vous rendez pas compte de la performance de ces petites machines qui n'ont pas grand chose à envier à des dual core de dix ans ou à des APU basse consommation comme les Atom ou les Kabini.
La limitation de puissance pour des logiciels très gourmands existe mais avec un Raspberry Pi 2 ou 3 on peut déjà faire beaucoup de choses, même du jeu en réseau ou de l'émulation donc peu de soucis de fluidité pour de la bureautique ou du surf si on fait gaffe à l'occupation en RAM.

On parle de faire un client léger. Sur du X en remote, c'est le serveur qui mouline les applis pas le client. Du coup, la puissance dont on a besoin côté client est vite contrecarrée par les latences réseau.
Si le réseau permettait un débit supérieur aux capacités du CPU, on est d'accord qu'il faudrait de la puissance mais là, on ne parle pas de ça.
En X Remote avec les machines actuelles, c'est le réseau qui est le goulet d'étranglement pas la puissance du CPU. On faisait déjà tourner des clients X sur des bécanes à peine plus puissantes qu'un grille-pain d'aujourd'hui.

Le soucis majeur de ce matériel réside dans son support de stockage système uniquement en microSD dont l'usure est bien plus importante qu'avec un SSD. En plus pour éviter les latences, il faut prendre une carte SD rapide (donc encore plus chère que les basiques) et faire attention au gros problème de contrefaçon de ce marché.
Cette usure peut toutefois se limiter en ne laissant que l'essentiel pour le boot et en déportant le reste sur USB (ou SATA sur certaines cartes ARM) et le reste sur un serveur mais là aussi il y a augmentation de la latence.

Encore hors sujet, on parle d'un client X qui n'a, donc par définition, qu'un besoin très limité de stockage. En gros, de quoi avoir un boot PXE.
Du coup, une microSD suffit largement

Ben, non, tu n'as que l'accès au GPU local à ton client léger.

Pour faire une bécane dédiée au surf, c'est largement suffisant.
Clairement pour jouer, il faut un accès direct, ne serait-ce que pour une histoire de latence réseau.

On ne peut pas déjà faire tourner un client léger sur un Rpi et utiliser la machine puissante comme serveur XDMCP ?
Si la machine est vraiment puissante, on peut, du coup, mettre quelques Pi sur le même réseau et refaire les bonnes vieilles classes de TP qu'on connaissait dans les 90's :D

Demain, je ne publie plus mes journaux que dans des images !!

C'était déjà du recyclage ☺

Les différences :

• Ada n'est pas autant multi-paradigme que peut l'être OCaml. On fait soit de l'impératif, soit de l'objet mais pas de fonctionnel
• Ada ne fait pas d'inférence de types (et encore moins d'autoboxing si on veut comparer à Java
• Ada est un langage normalisé par l'ISO sous la référence ISO/IEC 8652:2012(E) dont la norme est libre d'accès

Les atouts :

• Le langage contient déjà énormément de choses comme je l'ai déjà écrit plus haut
• Il est multi-plateforme car la norme ne tient pas compte des différences d'architecture. Cependant comme c'est un langage natif compilé, il faut obligatoirement un compilateur pour la plateforme cible

Pour les points communs, je ne peux pas dire, je ne connais pas OCaml.