Il y a aussi le fait que l'on est souvent bien plus libre sous windows que sous linux…
Quand on est pas root sous linux, cela veut dire qu'il est impossible de configurer sa machine comme on le veut, avec les applications que l'on veut.
Avec windows, 90% du temps tu installes le logiciel qui te plait. Avec un linux classique, c'est impossible.
Mandriva avait tenté le urpmi (u pour user) mais des clients (administrateur système donc) avait refusé le principe.
Le truc hallucinant en 2017, est d'avoir un firefox qui ne se met pas à jour tout seul avec l'infra mozilla, mais de dépendre de la distribution. Si il y un problème de cloisonnement, docker proposer déjà un début de solution.
Si tu va chercher une version plus récente de ton application, est-ce que ton gestionnaire ne va pas aussi tirer la mise à jour des dépendances, et donc la mise à jour des applications autres dont ils dépendent ?
C'est aussi les états qui ont demandé 6 ans de dev (au lieu de 10) pour un avion qui n'a jamais été fait (l'A400M est un très gros porteur à hélice), confié aux espagnols qui n'ont jamais été maitre d'oeuvre d'avion…
Vous pouvez aussi mettre une clef cryptographique dedans pour le TLS ou autre, le genre de clef qui est sur une étiquette sur la machine. Le principe est que seul une personne pouvant voir physiquement la machine au moins une fois, peut avoir accès à la clef. Cela me fait penser aux clefs WPA derrière les box wifi.
Ce serveur web ne tourne qu'au boot et disparait ensuite, non ? Il pourrait tourner dans un réseau différent de "la prod", c'est impossible de faire un vpn de "configuration" ?
Quand tu dis "absurdes", est-ce que tu connais bien les points de droit en relation ? Parce que souvent, il y a des trucs absurdes qui proviennent de trucs de base comme la recherche a tout prix d'un responsable. Parfois, il y a des responsabilités plus facile à démontrer que d'autres, même si cela parait absurde (quand des enfants sont impliqués par exemple).
Vu que ces remboursement de frais sont pour les personnes injustement accusés, je ne vois pas le rapport avec le fait de baisser le recourt à la justice.
Il ne parle pas des sources. Ce qu'il y a "autour" n'a rien de problématique. Mais bon en dessous, il est dit qu'ils reversent leur patch à gcc à la FSF, donc, il n'y a pas de problème.
Je n'ai jamais vraiment regarder les détails, mais il me semble que adacore "reprends" le code de gnat, le compilateur ada de gcc. Ils en ont fait une version propriétaire avec support. Mais bon, le code de gcc n'est-il pas en GPL à la base ?!
Oui, c'est bien ce que je dis, la migration est lente. Si je me souviens bien, un CPU dans la norme DO est considéré comme valide sans plus de preuves que cela s'il est monocoeur et ne réorganise pas l'ordre des instructions… Ce qui est de plus en plus rare aujourd'hui.
Il n'y a rien de tel dans la norme. Elle est justement très peu technique et parle surtout de processus de fabrication. Le cpu typique est le powerPC 601 qui fait un peu d'out of order, il me semble.
Ce cas de figure n'est pas vraiment documenté dans les standards aéro, et ils ont globalement 20 ans de retard sur ce qui est considéré comme standard. Ce qui est un soucis pour introduire bien sûr des calculs plus puissants pour le contrôle de l'appareil.
Projet assez génial on dirait :) Pour moi votre difficulté serait de faire valider tout le runtime qui est vendu avec ce genre de machin. Cela peut être extrêmement complexe. Le pire est le compilateur. Comment prouver que ce qui est compiler est correct, si vous n'avez pas la description de l'assembleur qui va avec ?
Pour les compilo C, on est censé prouver que le compilo génère le bon code objet. Cela a dû se faire par relecture et traçabilité entre code ASM et code C, mais maintenant, cela doit pouvoir se faire avec des exemples de code C à compiler, puis ensuite, on dit que tout code sera issue de ces blocs de base. Mais avec les trucs proprio NVIDIA, je ne vois pas comment faire ça. Vous avez regardez les "array de cpu" comme ceux de Kalray ?
Je n'en suis pas sûr, quand je m'y étais un peu intéressé il semblait impossible de pouvoir (mathématiquement) faire le langage parfait qui puisse exprimer n'importe quel programme de manière assez simple et en garantir la preuve de son bon fonctionnement.
Mais non, je parle de formaliser la DO178, elle-même, pour inclure dans un langage toutes les étapes décrites dans la norme. Le compilateur ne ferait que vérifier la cohérence de l'ensemble des informations (type traçabilité spec<->code<->test<->couverture de test, vérification de la couverture, etc…).
Cela revient à faire un langage qui impose une spec, le teste, la traçabilité et des revues.
Pour info, j'ai fais uniquement du DAL A (code qui vole, générateur de donné, outils de validation). Les démonstrations formelles ne sont pas accepté, en DO178b, et commence à l'être en DO178c. Le problème principale est que l'outil de validation lui-même doit être écris en DAL A pour être accepté.
SCADE est souvent utilisé dans les fadec, mais il n'y a aucune "preuve". Le langage est formel dans le sens ou il ne comporte pas d’ambigüité. Et le compilo est certifié.
D'ailleurs pour les DAL >= C, il devient difficile d'employer des CPU multi-cœurs ou avec un GPU moderne tellement que c'est contraignant vis à vis des normes.
Cela commence tout doucement. La première version de vxworks multicpu, tournait avec 2 instances d'OS, comme si il y avait 2 ordinateurs. C'est très compliqué de calculer le temps d’exécution avec ce genre de machine (ex: il y a une perte de perf de 20% sur les 2 cpu à cause de l'usage du bus mémoire). Si tu prends des marges de fou, avoir 2 cpu n'a plus trop d’intérêt.
Mais la mode IMA, c'est de tout "virtualiser" plus ou moins statiquement. Leur rêve est d'avoir des racks standards et de mettre les applications sur les ordinateurs fonctionnelles.
Concernant les GPU, je n'ai pas encore vu de code certifié. En graphique, il utilise de l'openGL SC, genre d'opengl 1.0, je crois que la dernières version a simplement pris l'api opengl ES vu comme plus propre. Il n'y a pas de shader la-dedans (il faudrait qualifier le compilateur…).
A part ça, je suis persuadé qu'il doit être possible de pouvoir créer un langage qui respecte toutes les contraintes de la DO178b, de le bootstraper et ensuite de pouvoir écrire plus facilement des applications qualifié. Mais cela va au-delà du code pure, car il faut gérer la documentation (les revues de code humaine, les descriptions api, le rapport d'architecture), les versions, les tests (et leur couverture), la traçabilitée.
Globalement la qualité se résume souvent à un cahier de tests, avec des tests unitaires ou fuzzing sans oublier la revue de code et l'intégration continue. Quand tu as ça, déjà, tu es content.
Tu voudrais quoi de plus ? C'est déjà pas mal. Dans l'aéronautique, ils n'ont pas de fuzzer, mais ont des revues de testes.
Typiquement en aéronautique cela sera exigé / recommandé pour les DAL A ou B, mais pas au delà.
Tu fais références à quoi ?
D'autant que si ton programme a un lien fort avec ton matériel (cas du noyau ou d'un logiciel embarqué), il faut aussi formaliser le matériel et cette liaison. Est-ce que des processeurs ou GPU modernes bénéficient d'un tel travail ? J'en doute.
Il te répond avec un langage qui fait cela pour du code sur GPU, et tu réponds que ça ne te parle pas ? C'est quoi le problème ? Qu'ils utilisent la lettre \lambda pour définir des fonctions ? Qu'ils écrivent reduce et non fold ?
Attention ne de pas tout mélanger. Le journal est a propos de la qualité des langages, de leur "ergonomie". Un des principes de l'ergonomie est le principe de "moindre surprise". Trouver un langage utilisant des caractères qui ne sont même pas présent sur un clavier, c'est "surprenant".
A force d'explication, personnellement, je comprends le lien entre lambda/map/fold/reduce, mais je pensais plus général, à l'acceptation du langage dans un cadre bien plus large.
Je ne suis pas sûr que la concision soit le principal moyen pour arriver à la "clarté".
[^] # Re: Détail du système + cout
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Retour d'expérience d'une petite administration sous linux depuis 8 ans qui fait marche arrière. Évalué à 6.
Il y a aussi le fait que l'on est souvent bien plus libre sous windows que sous linux…
Quand on est pas root sous linux, cela veut dire qu'il est impossible de configurer sa machine comme on le veut, avec les applications que l'on veut.
Avec windows, 90% du temps tu installes le logiciel qui te plait. Avec un linux classique, c'est impossible.
Mandriva avait tenté le urpmi (u pour user) mais des clients (administrateur système donc) avait refusé le principe.
Le truc hallucinant en 2017, est d'avoir un firefox qui ne se met pas à jour tout seul avec l'infra mozilla, mais de dépendre de la distribution. Si il y un problème de cloisonnement, docker proposer déjà un début de solution.
"La première sécurité est la liberté"
[^] # Re: Debian
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Retour d'expérience d'une petite administration sous linux depuis 8 ans qui fait marche arrière. Évalué à 5.
Si tu va chercher une version plus récente de ton application, est-ce que ton gestionnaire ne va pas aussi tirer la mise à jour des dépendances, et donc la mise à jour des applications autres dont ils dépendent ?
"La première sécurité est la liberté"
[^] # Re: Oui monsieur
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Ambassadeur pour le Numérique. Évalué à 7.
Est-ce que l'on rabaisse la puissance de ces boites quand on leur créait un poste d'ambassadeur pour dialoguer avec eux ?
"La première sécurité est la liberté"
[^] # Re: stupide
Posté par Nicolas Boulay (site web personnel) . En réponse au journal ils l'ont voulu, ils l'ont obtenu, et ils l'ont dans le baba.... Évalué à 3.
Je parlais des équipes d'EADS.
"La première sécurité est la liberté"
[^] # Re: stupide
Posté par Nicolas Boulay (site web personnel) . En réponse au journal ils l'ont voulu, ils l'ont obtenu, et ils l'ont dans le baba.... Évalué à 6.
C'est aussi les états qui ont demandé 6 ans de dev (au lieu de 10) pour un avion qui n'a jamais été fait (l'A400M est un très gros porteur à hélice), confié aux espagnols qui n'ont jamais été maitre d'oeuvre d'avion…
"La première sécurité est la liberté"
[^] # Re: Anthropisation
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Taxe béton Nicolas Hulot. Évalué à 4.
Dans le BTP, c'est plutôt l'inverse.
"La première sécurité est la liberté"
[^] # Re: Distribue les à tes projets préférés !
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Que faire avec ses clefs steam inutilisées ?. Évalué à 5.
Cela serait plus utile de les filer au projet que tu détestes. :)
Je sens que les développeurs de Systemd vont crouler sous les clefs…
"La première sécurité est la liberté"
[^] # Re: comme le cloud ?
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Vers des serveurs libres, ouverts et sécurisés : NERF (2). Évalué à 5.
Colles un ssh dans le bios dans ce cas, la "surface d'attaque" est simple, connu et sécurisé.
"La première sécurité est la liberté"
[^] # Re: comme le cloud ?
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Vers des serveurs libres, ouverts et sécurisés : NERF (2). Évalué à 4.
Vous pouvez aussi mettre une clef cryptographique dedans pour le TLS ou autre, le genre de clef qui est sur une étiquette sur la machine. Le principe est que seul une personne pouvant voir physiquement la machine au moins une fois, peut avoir accès à la clef. Cela me fait penser aux clefs WPA derrière les box wifi.
"La première sécurité est la liberté"
[^] # Re: comme le cloud ?
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Vers des serveurs libres, ouverts et sécurisés : NERF (2). Évalué à 3.
Ce serveur web ne tourne qu'au boot et disparait ensuite, non ? Il pourrait tourner dans un réseau différent de "la prod", c'est impossible de faire un vpn de "configuration" ?
"La première sécurité est la liberté"
# comme le cloud ?
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Vers des serveurs libres, ouverts et sécurisés : NERF (2). Évalué à 3.
Niveau interface, j'imagine que la gestion des clouds peut être une bonne source d'inspiration.
La mode est au API, comme celle d'AWS ou au conteneur type docker. Je dis une connerie ?
"La première sécurité est la liberté"
[^] # Re: l'assignation ne va jamais venir
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 6.
Quand tu dis "absurdes", est-ce que tu connais bien les points de droit en relation ? Parce que souvent, il y a des trucs absurdes qui proviennent de trucs de base comme la recherche a tout prix d'un responsable. Parfois, il y a des responsabilités plus facile à démontrer que d'autres, même si cela parait absurde (quand des enfants sont impliqués par exemple).
"La première sécurité est la liberté"
[^] # Re: l'assignation ne va jamais venir
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 10.
Vu que ces remboursement de frais sont pour les personnes injustement accusés, je ne vois pas le rapport avec le fait de baisser le recourt à la justice.
"La première sécurité est la liberté"
[^] # Re: adacore et GPL ?
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Retour d'expérience et présentation d'Ada dans le contexte d'une appli audio. Évalué à 3.
Il ne parle pas des sources. Ce qu'il y a "autour" n'a rien de problématique. Mais bon en dessous, il est dit qu'ils reversent leur patch à gcc à la FSF, donc, il n'y a pas de problème.
"La première sécurité est la liberté"
[^] # Re: adacore et GPL ?
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Retour d'expérience et présentation d'Ada dans le contexte d'une appli audio. Évalué à 4.
Cela veut dire que le code de GNAT pro est donné à ses clients payant, et qu'ensuite le code est reversé dans le code de gcc chaque année ?
"La première sécurité est la liberté"
# adacore et GPL ?
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Retour d'expérience et présentation d'Ada dans le contexte d'une appli audio. Évalué à 4.
Je n'ai jamais vraiment regarder les détails, mais il me semble que adacore "reprends" le code de gnat, le compilateur ada de gcc. Ils en ont fait une version propriétaire avec support. Mais bon, le code de gcc n'est-il pas en GPL à la base ?!
"La première sécurité est la liberté"
[^] # Re: l'assignation ne va jamais venir
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 5.
J'ai l'impression que les juges donnent rarement plus de 700 à 1000€, on est très loin des frais réels. Je ne comprends pas pourquoi d'ailleurs.
"La première sécurité est la liberté"
[^] # Re: l'assignation ne va jamais venir
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 5.
~ 1500€ pour une première instance. Si cela dure avec appel, expertise et autre, cela peut monter à 5/10 k€.
"La première sécurité est la liberté"
[^] # Re: Dommages
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 4.
Ce n'est pas une contrefaçon d'une œuvre qui n'est pas orignal publié avant son propre billet (si on en croit un autre commentaire)
"La première sécurité est la liberté"
[^] # Re: on vit une époque formidable
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Comment bloquer 280M de dollars en éther . Évalué à -8.
C'est le début d'etherum. Les avions n'ont pas commencé à voler avec peu de carburant pour transporter 150 personnes à 800 hm/h à 20 000 km.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Il n'y a rien de tel dans la norme. Elle est justement très peu technique et parle surtout de processus de fabrication. Le cpu typique est le powerPC 601 qui fait un peu d'out of order, il me semble.
Projet assez génial on dirait :) Pour moi votre difficulté serait de faire valider tout le runtime qui est vendu avec ce genre de machin. Cela peut être extrêmement complexe. Le pire est le compilateur. Comment prouver que ce qui est compiler est correct, si vous n'avez pas la description de l'assembleur qui va avec ?
Pour les compilo C, on est censé prouver que le compilo génère le bon code objet. Cela a dû se faire par relecture et traçabilité entre code ASM et code C, mais maintenant, cela doit pouvoir se faire avec des exemples de code C à compiler, puis ensuite, on dit que tout code sera issue de ces blocs de base. Mais avec les trucs proprio NVIDIA, je ne vois pas comment faire ça. Vous avez regardez les "array de cpu" comme ceux de Kalray ?
Mais non, je parle de formaliser la DO178, elle-même, pour inclure dans un langage toutes les étapes décrites dans la norme. Le compilateur ne ferait que vérifier la cohérence de l'ensemble des informations (type traçabilité spec<->code<->test<->couverture de test, vérification de la couverture, etc…).
Cela revient à faire un langage qui impose une spec, le teste, la traçabilité et des revues.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Pour info, j'ai fais uniquement du DAL A (code qui vole, générateur de donné, outils de validation). Les démonstrations formelles ne sont pas accepté, en DO178b, et commence à l'être en DO178c. Le problème principale est que l'outil de validation lui-même doit être écris en DAL A pour être accepté.
SCADE est souvent utilisé dans les fadec, mais il n'y a aucune "preuve". Le langage est formel dans le sens ou il ne comporte pas d’ambigüité. Et le compilo est certifié.
Cela commence tout doucement. La première version de vxworks multicpu, tournait avec 2 instances d'OS, comme si il y avait 2 ordinateurs. C'est très compliqué de calculer le temps d’exécution avec ce genre de machine (ex: il y a une perte de perf de 20% sur les 2 cpu à cause de l'usage du bus mémoire). Si tu prends des marges de fou, avoir 2 cpu n'a plus trop d’intérêt.
Mais la mode IMA, c'est de tout "virtualiser" plus ou moins statiquement. Leur rêve est d'avoir des racks standards et de mettre les applications sur les ordinateurs fonctionnelles.
Concernant les GPU, je n'ai pas encore vu de code certifié. En graphique, il utilise de l'openGL SC, genre d'opengl 1.0, je crois que la dernières version a simplement pris l'api opengl ES vu comme plus propre. Il n'y a pas de shader la-dedans (il faudrait qualifier le compilateur…).
A part ça, je suis persuadé qu'il doit être possible de pouvoir créer un langage qui respecte toutes les contraintes de la DO178b, de le bootstraper et ensuite de pouvoir écrire plus facilement des applications qualifié. Mais cela va au-delà du code pure, car il faut gérer la documentation (les revues de code humaine, les descriptions api, le rapport d'architecture), les versions, les tests (et leur couverture), la traçabilitée.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Tu voudrais quoi de plus ? C'est déjà pas mal. Dans l'aéronautique, ils n'ont pas de fuzzer, mais ont des revues de testes.
Tu fais références à quoi ?
Il n'y a pas d'étude formelle, mais il y a une norme à respecter https://fr.wikipedia.org/wiki/DO-254
"La première sécurité est la liberté"
[^] # Re: Trop génial ! Une base de données légale.
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Atelier Barcamp I. A. & Droit le 7 novembre 2017 à Paris. Évalué à 3.
"La première sécurité est la liberté"
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Attention ne de pas tout mélanger. Le journal est a propos de la qualité des langages, de leur "ergonomie". Un des principes de l'ergonomie est le principe de "moindre surprise". Trouver un langage utilisant des caractères qui ne sont même pas présent sur un clavier, c'est "surprenant".
A force d'explication, personnellement, je comprends le lien entre lambda/map/fold/reduce, mais je pensais plus général, à l'acceptation du langage dans un cadre bien plus large.
Je ne suis pas sûr que la concision soit le principal moyen pour arriver à la "clarté".
"La première sécurité est la liberté"