Le 12/11/2019 à 09h 43

Merci Amazon ! C’est vrai que c’est super fatiguant le libre arbitre, devoir façonner sa vie soi-même, tout ça.

Le 16/09/2019 à 10h 00

<Insérer un commentaire sur l’usage d’outils formels en info ici>

Le 04/03/2019 à 12h 23

RévolutioN a écrit :



  … la marque sans aucuns bugs ni failles qu’elle était autrefois.





Pour rappel, les jailbreaks d’iPhone qui étaient monnaie courante pendant les années Jobs exploitaient des failles et des bugs dans iOS ou les appareils. Donc on est loin du “sans faille”.

Le 16/11/2018 à 10h 16

J’ai déjà suffisamment à faire avec Murphy pour ne pas m’intéresser à Machiavelli " />

Le 15/11/2018 à 12h 02

Burn2 a écrit :



En gros à quoi sommes nous vulnérables et quel est l’inpact. Que faire pour s’en protéger etc?

Quid des différences entre les os sur le degré de correction?





Pas d’inquiétude. De toute façon, le reste du code est tout aussi plein de failles critiques.

Le 15/11/2018 à 12h 05

Azerty38 a écrit :



“et fiancé par la Commission européenne” le mariage c’est pour quand ?





Quand ça représentera la majorité du financement sur toutes les autres activités sans doute.

Le 14/11/2018 à 12h 06

Je dois dire que même si je ne suis toujours pas enthousiaste, ce nouveau trailer m’inquiète moins. Les plans sur la décharge laissent transparaître un peu plus ce qu’on trouvait dans le manga (bon c’est pas fou hein). Et même si ça ne suit manifestement pas l’histoire directement, ça semble pas trop absurde dans le choix des personnages.

L’humeur qui ressort d’Alita ressemble par certains aspects à ce qui a été fait dans le prolongement avec LastOrder (“vous faites l’erreur de me sous-estimer”, en gros).

Mais par contre pour l’aspect philosophique à mon avis, on va pouvoir se le mettre au c…

Le 24/10/2018 à 18h 41

tmtisfree a écrit :



Quand il sortira, s’il sort un jour, il sera en retard de dix ans parce que les autres seront à cent fois plus de qubits (DWave a un QPU à 2000 qubits depuis 2017).

Sauf que visiblement, ça se bat assez sévèrement pour déterminer si les  machines de DWave sont effectivement des ordinateurs quantiques ou s'ils exploitent simplement des mécanismes quantiques sans pour autant avoir  tout ce qu'il faut.     

Pour comparaison, IBM, Intel et Google sont super fiers d’avoir des machines maison avec resp. 50, 49 et 72 qbits.



 





tmtisfree a écrit :



Qui va croire que c’est en recherchant/concevant sur 100 qubits qu’on va pourvoir automatiquement avoir des réponse de la faisabilité à 1 M ? Par modélisation, extrapolation ou autre esbroufe à la mode en pseudoscience ?



 

Globalement, le CNRS et le CEA c’est pas des glandus non plus en recherche.

Le 25/09/2018 à 11h 46

empty a écrit :



Le numérique et le digital, c’est quoi la différence ?





Le premier ce qui a trait au numérique, le second ce qui a trait aux doigts. Ça paraît évident " />

Le 09/09/2018 à 16h 52

JFP285 a écrit :



On parle aussi de “pre-print” ou de “prépublication”. Souvent les chercheurs mettent ces versions sur leurs pages personnelles sur HAL, ou ResearchGate, Academia… Mais je ne suis pas sûr que ce soit autorisé par toutes les revues.





Ce n’est pas du tout autorisé par la plupart des revues. Le concept c’est justement de ne pas mettre directement ces versions sur son site personnel mais uniquement des liens HAL. De cette manière c’est eux qui re-distribuent un contenu plus ou moins sous copyright (modulo mise en page finale) et pas toi.



Pour le reste, c’est la triste constatation. Mais ça commence à chauffer dans les chaumières, en Allemagne par exemple, et il y a des regroupements de chercheurs en France qui cherchent à suivre un chemin similaire.



Les revues c’est vraiment le summum du what the fuck qu’on accepte parce qu’on nous pousse à publier sur des trucs connus. Les mecs font littéralement RIEN, quand il y a un soucis d’après leur système automatique, c’est toi qui doit le régler, même quand c’est une merde dans leur template. Eux, concrètement, ils empochent l’argent et voilà. Parce que même imprimer ça se fait de moins en moins (encore heureux).

Le 07/09/2018 à 21h 53

Ouais enfin, il faut pas oublier que le concept de HAL jusqu’à maintenant, est de mettre les versions finales “auteur” de l’article (donc pas la version finale “publisher”) sur la plateforme afin que ce soit HAL qui gère les embrouilles de droit si besoin.



Donc un système qui permet d’éviter ce bordel serait pas plus mal.

Le 08/01/2018 à 13h 47

Non puis niveau centralisation Facebook c’est quand même un cas d’école. Il y a des gens chez qui on pourrait renommer le navigateur Facebook, voir carrément mettre un bouton facebook plutôt que Power sur la machine.

Le 20/06/2017 à 12h 18

Si LDLC pouvait arrêter de bouffer tout ce qui bouge et revenir à la qualité de service qu’elle avait il y a quelques années, ce serait probablement plus utile. Notamment en ce qui concerne ses choix de service de livraison …

Le 15/06/2017 à 12h 15

> Vous avez 3 min et l’envie d’entendre parler de science ? – Depuis quelques années déjà, le CNRS et la CPU (Conférence des présidents d’université) organisent Ma Thèse en 180 secondes.



Ouais enfin, c’est plus sur un format commerce/publicité que de la science, vu que c’est même tout le concept de l’exercice.

Le 07/04/2017 à 16h 20

Le but principal n’est pas d’avoir du code utilisable, le but est d’avoir du code qui puisse être lu et exploré. Ensuite, si les moyens suivent, si, on pourra continuer à avoir du code qu’on peut exécuter, car justement l’idée est d’embarquer les dépendances, les versions d’environnement, etc …



 Quant au troll, il n’est pas très imaginatif.

Le 27/03/2017 à 09h 51

Il va plus y avoir beaucoup de permis.

Le 20/03/2017 à 10h 34

Oulanos a écrit :



En attendant nous pouvons jouer à Elite dangerous ;)





Je pense que le choix de Frontier d’avoir fourni rapidement du contenu jouable (même si le jeu ne prends définitivement pas le joueur par la main pour lui donner envie de s’investir dedans) était une bonne idée. Ce qui m’inquiète par rapport à Star Citizen, c’est qu’on a presque l’impression que d’ici sa sortie, ED contiendra le contenu initialement prévu pour SC.

Le 04/03/2017 à 16h 36

C’est pas beau de se moquer d’un correcteur de frappe.

Le 04/03/2017 à 14h 53

4RB-bzh- a écrit :



Donc avant de nous pomper notre fric pour 1 malheureux km/h de plus que la limitation, …





On parle de +10% à +10km/h sur ces radars, pour 90km/h, ça fait pas loin de ¹⁰²⁄₅ km/h à l’affichage du compteur selon le véhicule.



Cela dit la remarque sur l’usage des clignotants, l’usage du téléphone, le placement sur les voies (particulièrement les sens giratoires) et les priorités reste vraie.

Le 04/03/2017 à 14h 39

Fais toi faire des lunettes à verts jaunes. Ça réduit très fortement l’éblouissement et augmente les contrastes, c’est genre parfait pour la conduite de nuit. (Mais des VRAIES : catégorie 1 et fournies par un opticien, pas les trucs 5 balles sur le marché).

Le 24/02/2017 à 14h 52

Il ne sont pas dans la liste montrée sur la page Github. Ce qu’il faut regarder c’est le contenu du fichier, qui est LARGEMENT plus conséquent.

Le 24/02/2017 à 14h 48

Quand je parle de vérification formelle de composants de sécurité, je pense plutôt à des trucs comme ça :

• https://eprint.iacr.org/2016/846.pdf
  


• https://people.csail.mit.edu/nickolai/papers/chong-nsf-sfm.pdf
  
  
  
  Bref, quelque chose de très amont, qui donne des garanties très fortes en terme de sûreté et de sécurité, mais qui demande une débauche de temps et de moyens assez conséquente.

Le 24/02/2017 à 14h 31

Je ne sais pas si on parle de la même chose quand j’écris “formellement vérifié”. Cela ne court définitivement pas les rues les systèmes de ce genre (malheureusement).

Le 24/02/2017 à 14h 14

Ce serait bien qu’un jour les composants de sécurité écrits en C soit vérifiés formellement. Ou plus écris en C. UN jour, peut être, s’il y a de l’argent.

Le 23/02/2017 à 08h 31

Personnellement, j’attends surtout les 6 coeurs pour avoir de quoi choisir entre i5 et R5. Mon Phenom commence à saturer dans certain jeux et je crois que ma CM est à bout de souffle.

Le 20/02/2017 à 14h 32

En même temps ces classements sont plutôt imprécis et le TIOBE, ‘fin bon quoi. A la limite, le IEEE Spectrum est un peu moins naze que les autres. D’ailleurs on y trouve le D pas si mal placé dans l’embarqué.

Le 14/02/2017 à 13h 49

Pas réussi à reproduire le bug sur un 950.



Bon cela dit, mon écran verrouillé n’a pas de sécu, donc ça n’a pas grande importance.

Le 13/02/2017 à 10h 31

Il faut que j’aiguise un peu plus mon second degré à l’écrit je crois.

Le 13/02/2017 à 09h 46

garn a écrit :



qu’est ce que tu as contre Rock Simulator? C’était très bien Rock simulator





Fallait bien avoir une alternative un peu différente à Rocksmith et RockBand

Le 02/02/2017 à 19h 28

Je ne savais même pas qu’on pouvait utiliser autre chose que LaTeX pour une thèse.

Il y a des doctorants bizarres quand même.

Le 17/01/2017 à 10h 52

En truc démentiel au niveau utilisation d’énergie inutile (je parle au niveau utilisateurs lambdas hein), il y a l’usage des vidéos youtube pour écouter de la musique.

Le 13/01/2017 à 09h 16

Sans péage alors " />

Le 06/01/2017 à 15h 58

RomRomRomRom a écrit :



(1) Si j’ai tout compris, les enfants qui n’existent pas (ceux qui n’ont pas été conçus) sont les plus heureux parce qu’ils ont jamais été obligés de rien ?



(2) C’est vraiment ta pensée ou tu te fais l’avocat du diable ?



(3) En vrai, je crois que je comprends ce qui te dérange, le fait de ne pas avoir choisi, qu’on t’impose quelque chose que tu peux difficilement changer.



(4) comment tu fais pour ne pas déprimer ? Tu essaies de t’entourer seulement de tes propres (bonnes) décisions afin d’oublier le reste ? Ça marche ?







(1) Ben non, ils existent pas, donc ils peuvent pas être heureux. Ils ne sont pas. C’est tout. En tout cas, c’est clair qu’ils sont pas malheureux.



(2) La question m’amuse, c’est tout. C’est un peu la continuité de “est ce que c’est triste de mourir ?”. Pour toi, non, évidemment, c’est pour les autres que c’est triste. Donc la continuité, “est ce que donner la vie c’est un cadeau ?” ben non, c’est juste que t’es vivant, tu serai pas plus malheureux si tu ne l’étais pas. Alors ce serait quand même un comble qu’on te demande d’être reconnaissant.

 

(3) Oh, il y a pleins de trucs qui me dérangent, ça non.



(4) L’ironie. Ça marche du tonnerre !

Le 06/01/2017 à 15h 12

RomRomRomRom a écrit :



(1) […] les orphelins […] s’en sortent bien mieux, une fois libérés de cette oppression insoutenable. " />



[…] enfants de parents divorcés […] sont exaltés toute leur vie par cette insufflation de libre arbitre précoce.  



(2) Prenons un exemple : tu trouves mieux de “mourir de faim” plutôt que d’être “obligé de dire merci parce qu’on te donne gratuitement une pomme” ? 





(1) Note que s’ils n’étaient pas né. Ils n’auraient pas ces questions à se poser. C’est précisément ça le truc. Le choix qu’on t’impose en premier, c’est surtout celui là.



(2) Avant ou après le décès ? Parce que après, techniquement, tu t’en fous pas mal.



 L’exemple c’est plutôt : quelque soit ce que tu avais, tu ne l’as plus et on t’offre une maison avec un jardin, que dont tu ne peux pas te débarrasser et qui sont ton seul moyen de vivre. Ensuite on t’apprend à t’en servir correctement et là tu dis merci. Sauf qu’en premier peut être que la maison et le jardin, t’en voulais pas.

 

Le 06/01/2017 à 13h 41

1. Choix ou connerie, la conséquence de base est la même, c’est surtout au collatéral que ça change.
   
   
   
   
   
   
   
   1. Non, je les ai mangés,  ça évite de faire des papiers.
      
      
      
      Sur un plan strictement personnel je m’en fous un peu. C’est juste que je trouve amusant cette sorte de volonté admise à dire que si des parents ont bien élevé et permis d’avoir une bonne situation à un gamin, il doit leur être reconnaissant. “Bon t’as pas eu le choix, mais maintenant tu dis merci”.
   
   

Le 06/01/2017 à 12h 23

brazomyna a écrit :



La logique est qu’une famille est un groupe social et que chacun se doit d’y apporter sa contribution pour que ça tourne rond.





Ce qui revient profondément au même. Un gamin n’a jamais demandé à faire partie du groupe social qui est sa famille. Il assume le choix de ses parents.

Le 06/01/2017 à 12h 13

En même temps, il y a aussi une part malsaine là dedans. “Aide nous parce qu’on fait plein de trucs pour toi qui est notre enfant”. Réponse : “vous ne m’avez pas demandé mon avis avant de me concevoir, si j’étais pas là tu devrais bien te démerder”.

Le 30/11/2016 à 13h 46

> « Madame, Monsieur, votre attention, s’il vous plait. Suite à un

incident, notre TGV aura un retard d’une heure lors de son arrivée en

gare ». Qui prend plus ou moins régulièrement le train s’est très

certainement un jour ou l’autre retrouvé à entendre un message du genre



Je sais pas comment je me démerde, mais je suis à plus de 80% dans ce cas là sur mes voyages (et sans biais, c’est du réel là).

Le 23/11/2016 à 11h 12

Merci ! " />

Le 23/11/2016 à 10h 41

charon.G a écrit :



(1) Pour les performances j’ai déjà expliqué plusieurs fois que le projet midori basé sur un micro noyau safe était un système hautes performances plus rapide que Windows. tous les papiers et sources disponibles en parlaient.



(2) Ensuite le langage M# fonctionnait comme rust de plusieurs façons. Une bonne partie des vérifications se faisaient à la compilation grâce au compilateur bartok. Bartok effectuait tout un tas de vérifications dès la compilation. 



(3)  Il est écrit en rust un langage safe et effectuait le même genre d’optimisations que midori. Ou sont passés les personnes qui critiquaient les performances des langages safe quand quantum a été annoncé?  Au final quantum est beaucoup plus rapide que firefox avec seulement une partie du code en rust. Si les préjugés sur les performances du code safe avaient été fondés on aurait observé une nette baisse de performance mais ce n’est pas du tout le cas.

 

(4) Explique moi ça. parce que bon tu préfères peut être la situation actuelle où les drivers obtiennent les pleins privilèges sur la machine.







 (1) Il y a des articles côté MsResearch pour ça ? Je suis pas mal les travaux de Cohen, Leino et Bjorner, qui sont plus du côté formel, mais je n’ai jamais vu mention de Midori du côté de la communauté scientifique (et encore moins de M#).



(2) Pour Rust, avec Patina on aura bientôt une formalisation complète. Peut-être un futur CompCert-Rust en perspective " /> . Cela dit je n’ai pas fondamentalement de problème avec les langages moins vérifiés à la compilation si on a un analyseur statique qui permet de faire des vérifications sur le code avant de le compiler. Un point sur lequel Rust pourrait affiner un peu serait de rendre la propriété “unsafe” moins violente. Par exemple dans le CppGuidelines, un truc sympa est la possibilité de désactiver une vérification particulière plutôt que toutes les vérifications.



(3) Un code plus défini formellement, c’est toujours de l’information supplémentaire pour mieux optimiser. C’est pour ça que par exemple du côté de CompCert, il y a des travaux pour extraire de l’info sémantique supplémentaire à partir du code reçu (par exemple par interprétation abstraite) pour produire des optimisations plus fines. Après, se pose quand même la question de savoir quel est le pourcentage de code unsafe dans la partie Rust de Quantum.



(4) Pareil.

Le 22/11/2016 à 20h 57

Prouvé ne signifie pas complexe. C’est même plutôt l’inverse en fait. Donc sur le plan micronoyau, avec du budget, si, c’est de l’ordre du faisable en 14 années de faire un micronoyau prouvé (10k LOC). Sur le plan perf seL4 n’est pas mal du tout. Son problème c’est de n’être exécutable que sur un thread worker pour l’OS. Et si tu es prêt à laisser un tout petit peu de perf de côté, le cloisonnement obtenu est notable.



 Actuellement, les plus gros problème qu’il y a pour les preuves de micronoyau sur multi-coeur, outre la difficulté de la concurrence elle-même (déjà présente à un autre niveau sur mono-coeur), c’est surtout les modèles mémoire de processeur/langage. C’est pour ça que d’une part, il y a des travaux pour la vérification de programmes sous les modèles mémoires faibles côté langage (variantes de logiques pour ces modèles) mais également pour la création de compilateur prouvé et prenant en compte ces modèles dans leur preuve de correction (CompCert-TSO par exemple).

Le 22/11/2016 à 16h 26

On est pas encore vendredi " />

Le 22/11/2016 à 14h 32

Quel L4 ? ;) . L4 c’est une génération de micronoyau, mais il y en a une multitude sur ce modèle.

Le 22/11/2016 à 13h 55

Actuellement, le seul micro-noyau qui soit intégralement vérifié c’est seL4 et il reste “limité” à une preuve formelle pour une exécution mono-coeur du micronoyau. Je serai assez étonné que Kaspersky ait réussi le tour de force de faire la même chose les doigts dans le nez sans le hurler à toute la communauté scientifique.



Donc ça pue la grosse com avec peut être quelque chose de conséquent derrière mais probablement pas inviolable, en tout cas sans preuve d’inviolabilité.

Le 15/11/2016 à 10h 23

devyg a écrit :



aucun système n’est sûr et ne le sera jamais.





Pitié … Heureusement qu’on est foutu de construire des systèmes sûrs. Les vrais questions c’est les conditions de sûreté, son coût et l’environnement de déploiement.

Le 04/11/2016 à 08h 27

Loeff a écrit :



[…], digne d’un fist gravier verre pilé des plus violant.

Le jeu de mot était volontaire ?   

 

(EDIT : groumpf, la citation ne prend pas les mises en forme …)

Le 19/10/2016 à 11h 35

Ben si au lancement tu crâmes le truc que t’étais sensé envoyer, tu l’as un peu dans l’os concrètement, et tous les sous investis pour les phases suivantes sont aussi crâmés. Et c’est le point marrant que pointe ce passage d’un sketch de François Pérusse, où ils ont juste paumé le satellite, et pas crâmé, certes.

Le 19/10/2016 à 11h 14

Quand je lis un truc comme ça dans les news sur les lancements spatiaux :



> En effet, juste après avoir envoyé le module TGO (Trace Gas Orbiter) vers la planète Mars, le dernier étage de la fusée Proton-M a explosé.



A chaque fois je pense à :

• vous savez combien ça coûte ce satellite ?
  


• ah ze sais pas.
  


• 950M US incluant la mise en orbite
  


• ah bah là vous pouvez exclure la mise en orbite.

Le 06/10/2016 à 10h 29

Les illuminatis reptiliens recrutés comme agents doubles par Sylvanus.

Le 03/10/2016 à 10h 19

Récent … Façon de dire. La GTX960M est dispo depuis mars 2015 et la machine en elle-même est sortie en février. Pour le coup je suis content que la bêta de Ubuntu Gnome soit ouverte aux utilisateurs.



Quant au choix machine/OS, c’est réfléchis. Si j’ai cette machine c’est parce que j’ai besoin de cette puissance et de cette mobilité (et je suis pas rothschild non plus). Et si je suis sous Nux quand je bosse c’est aussi parce que j’en ai besoin.