… 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”.
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…
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.
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).
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.
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.
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 …
> 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 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.
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.
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 102⁄5 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.
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é).
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.
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).
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.
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.
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é.
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.
(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.
(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.
Choix ou connerie, la conséquence de base est la même, c’est surtout au collatéral que ça change.
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”.
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.
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”.
(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.
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).
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é.
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.
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.
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.
197 commentaires
Le 12/11/2019 à 09h43
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 à 10h00
<Insérer un commentaire sur l’usage d’outils formels en info ici>
Le 04/03/2019 à 12h23
Le 16/11/2018 à 10h16
J’ai déjà suffisamment à faire avec Murphy pour ne pas m’intéresser à Machiavelli
" />
Le 15/11/2018 à 12h05
Le 15/11/2018 à 12h02
Le 14/11/2018 à 12h06
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 à 18h41
Le 25/09/2018 à 11h46
Le 09/09/2018 à 16h52
Le 07/09/2018 à 21h53
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 à 13h47
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 à 12h18
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 à 12h15
> 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 à 16h20
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 à 09h51
Il va plus y avoir beaucoup de permis.
Le 20/03/2017 à 10h34
Le 04/03/2017 à 16h36
C’est pas beau de se moquer d’un correcteur de frappe.
Le 04/03/2017 à 14h53
Le 04/03/2017 à 14h39
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 à 14h52
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 à 14h48
Quand je parle de vérification formelle de composants de sécurité, je pense plutôt à des trucs comme ça :
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 à 14h31
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 à 14h14
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 à 08h31
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 à 14h32
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 à 13h49
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 à 10h31
Il faut que j’aiguise un peu plus mon second degré à l’écrit je crois.
Le 13/02/2017 à 09h46
Le 02/02/2017 à 19h28
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 à 10h52
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 à 09h16
Sans péage alors
" />
Le 06/01/2017 à 15h58
Le 06/01/2017 à 15h12
Le 06/01/2017 à 13h41
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 à 12h23
Le 06/01/2017 à 12h13
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 à 13h46
> « 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 à 11h12
Merci !
" />
Le 23/11/2016 à 10h41
Le 22/11/2016 à 20h57
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 à 16h26
On est pas encore vendredi
" />
Le 22/11/2016 à 14h32
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 à 13h55
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 à 10h23
Le 04/11/2016 à 08h27
Le 19/10/2016 à 11h35
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 à 11h14
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 à :
Le 06/10/2016 à 10h29
Les illuminatis reptiliens recrutés comme agents doubles par Sylvanus.
Le 03/10/2016 à 10h19
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.