Il y a quand même des patterns connus pour prouver qu'un calcul distribué termine par exemple. On peut montrer aussi des propriétés d'autostabilisation ou des choses comme ça.
Je pense que tu t'égares :)
Que cela soit en distribué ou pas, on a un système que l'on modélise, une spec, un programme et des outils de preuves pour montrer que le programme est conforme à la spec, étant donné le système considéré.
Pour du code, généralement le système est connu : selon le langage tu as un jeu d'instructions, un système de type (c'est encore plus facile à formaliser/prouver, si ton langage a du typage fort), tu peux éventuellement modéliser la mémoire pour certains langages bas niveau et mettre 2/3 contraintes de QoS (puissance CPU, etc.), mais globalement cela s'arrête là.
Pour un système distribué, en plus d'avoir les contraintes d'implémentations, tu as les contraintes de distributions et de sécurité (cf. fautes byzantines), qui ajoutent des problèmes au niveau spécification. De tels problèmes sont connus, il s'agit par exemple de consensus distribué, de synchronisation en environnement asynchrone, d'authentification forte,…etc
Ce sont deux domaines différents, qui ont tous les deux des cas d'usage difficiles à prouver, mais ce que je veux te montrer c'est que si tu apportes de la distribution, tu apportes de la complexité dans le système, donc tout devient plus difficile à commencer par la spécification.
Pour finir :
Il y a quand même des patterns connus pour prouver qu'un calcul distribué termine par exemple. On peut montrer aussi des propriétés d'autostabilisation ou des choses comme ça.
Avec une modélisation juste d'Internet, c'est-à-dire un système distribué asynchrone dans lequel on ne sait pas distinguer le cas où une machine est lente à répondre ou si elle est en panne, tes propos sont faux. C'est un résultat théorique très connu dans le domaine de l'algorithmique distribué, on le nomme « FLP », pour « Fischer, Lynch, Paterson » et il dit en termes simplifiés :
On ne peut pas réaliser un consensus dans un système distribué asynchrone (modèle message passing) , si on tolère au plus une panne (réseau ou machine).
Ce qui signifie que non : on ne peut pas montrer qu'un consensus se termine ou qu'un système distribué se stabilise, c'est impossible ! Il existe bien entendu des astuces (se reposer sur un serveur centralisé qui fait fois), mais formellement on ne peut pas prouver ce genre de chose si on prend les hypothèses d'un réseau de type WAN.
T'es en train de dire que faire une spécification correcte est plus dur que faire du code incorrect ?
Oui, je t'invite à lire Paxos de Lamport justement, c'est un bon exemple de la complexité qu'un protocole (resp. qu'une spec.) peut avoir.
Attention, je ne dis pas qu'une implémentation est forcément simple, mais des fois (et c'est particulièrement vrai en algorithmique distribuée) la spécification est plus complexe que l'implémentation.
Je confirme que c'est de la fiction, car les productions scientifiques de Lamport et/ou de l'INRIA ne sont pas libres et c'est la guerre entre les labos de recherche. Cela dit, quand l'un a pondu l'article du siècle c'est une avancée qui profite à tous ! D'ailleurs Lamport a déjà bien fait avancer les choses dans le domaine de formalisation des protocoles distribués.
Pour ce qui est de la preuve, attention à ne pas confondre protocole et implémentation ! On peut très bien prouver plein de choses sur les protocoles SSL/TLS, ce qui n'empêchera pas leurs implémentations d'être buggées !
Je veux dire par là que dans la preuve du protocole, on suppose que les méthodes « send(message) » et « receive(message) » sont fiables. Si ce n'est pas le cas (comme pour SSL d'après ce que j'ai compris) la preuve ne tient plus :(
Je me rappelle avoir posé cette question à un chercheur dans le domaine de la vérification formelle : « What if the OS running your proved protocol didn't behave as expected ? Do you run your implementation on proved OS ? Do they run on proved CPU ?»
Je suis aussi tenté par fastmail, mais il y a un point sur lequel je doute : propose t-il aussi des noms de domaine ou serais-je obligé de changer d'adresse pour une adresse en « fastmail.fm » ?
J'ai lu en peu leur page de présentation et j'avoue que je n'arrive pas à me faire une idée clair, il parle de migration facile mais sans parler d'adresse ou de nom de domaine.
Officiellement je n'ai pas acheté du kimsufi, mais l'offre que j'ai y correspond. Il faudrait que je vérifie tout ça, mais je m'y perd dans tous ces noms marketing.
Mais c'est probablement l'ancien domaine lié à cette IP.
La date de blocage est très récente (< 3 jours) et j'ai ce domaine depuis plus d'un an, donc le problème est autre…
J'ai vérifié sur mon nom de domaine (hébergé chez OVH avec le mail associé) et j’apparais dans deux blacklist :
Chez CBL, je suis blacklisté à cause du site d'un hôtel parisien qui utilise la même adresse IP que moi (co-hébergé chez OVH ?).
Chez spamhaus, qui m'indique que l'IP du serveur mail est blacklisté, mais pas le nom de domaine. Du coup je ne sais pas trop si je suis vraiment blacklisté ou pas…
Du coup je suis dubitatif sur cette histoire de nom de domaine qui n'est pas le miens, mais qui fait que j'apparais quand même sur des blacklist.
C'est un problème qui normalement ne devrait pas arriver en auto-hébergement :)
C'est vrai que ce que j'entends par critique c'est le point de vue sécurité (bug = potentielle mort d'homme). Il est vrai que si tu as des contraintes temps réel cela peut changer, mais je n'ai jamais vu de tel code et il me semblait que l'aérospatial misait beaucoup sur Ada pour ce genre de chose notamment.
" rebinding Esc keyimap,,<Esc>noremap<C-s>:write<CR>inoremap<C-s><Esc>:write<CR>" {W} -> [É]" ——————————" On remappe W sur É :noremapéwnoremapÉWnoremapéé:VimwikiIndex<CR>" Corollaire, pour effacer/remplacer un mot quand on n’est pas au début (daé / laé)." (attention, cela diminue la réactivité du {A}…)noremapiéiwnoremapiÉiWnoremapaéawnoremapaÉaW" Pour faciliter les manipulations de fenêtres, on utilise {W} comme un Ctrl+W :"noremap w <C-w>"noremap W <C-w><C-w>" [HJKL] -> {CTSR}" ————————————————" {cr} = « gauche / droite »noremapchnoremaprl" {ts} = « haut / bas »noremaptjnoremapsk" {CR} = « haut / bas de l'écran »noremapCHnoremapRL" {TS} = « joindre / aide »noremapTJnoremapSK" Corollaire : repli suivant / précédentnoremapzszjnoremapztzk" {HJKL} <- [CTSR]" ————————————————" {J} = « Jusqu'à » (j = suivant, J = précédant)noremapjtnoremapJT" {L} = « Change » (l = attend un mvt, L = jusqu'à la fin de ligne)noremaplcnoremapLC" {H} = « Remplace » (h = un caractère slt, H = reste en « Remplace »)noremaphrnoremapHR" {K} = « Substitue » (k = caractère, K = ligne)noremapksnoremapKS" Corollaire : correction orthographiquenoremap]k]snoremap[k[s" Désambiguation de {g}" —————————————————————" ligne écran précédente / suivante (à l'intérieur d'une phrase)noremapgsgknoremapgtgj" onglet précédant / suivantnoremapgbgTnoremapgégt" optionnel : {gB} / {gÉ} pour aller au premier / dernier onglet"noremap gB :exe "silent!tabfirst"<CR>"noremap gÉ :exe "silent!tablast"<CR>" optionnel : {g"}pouralleraudébutdelaligneécran
C'est très dommage, car on y gagne vraiment (plus besoin de lever le poignet pour aller chercher les flèches). Et ça représente des kilomètres de parcourus sur une journée.
De toute façon, tant qu'on a pas vraiment essayé, on ne peut pas vraiment se rendre compte (c'est comme le bépo).
PS: bon le truc con c'est que c'est un mapping azerty/qwerty pour le jeux, mais si c'est juste pour « jklm », tu peux repasser en azerty juste pour le jeux et ensuite switcher dans vim sur « ctsr » :)
Par contre, ce qui est sûr, c'est que tous les gens que j'ai vu coder sur des trucs critiques n'utilisaient pas C, ou alors via des générateurs de code, comme c'est le cas notamment dans certaines branches de l'aéronautique.
Je suis d'accord cela ne convient pas à tous les postes. Je suis développeur et j'édite tout sur ma machine, y compris tout ce que je peux accéder via ssh (config sur serveurs, …etc). Je n'ai donc aucun problème de remapage, mais j'imagine que ce n'est pas le cas de tout le monde.
Quant aux machines des collègues, non je ne les remappe pas (je ne vois pas bien pourquoi je le ferais au passage). J'ai juste un clavier azerty pas loin à brancher sur ma machine en cas de besoin, et ça fait généralement l'affaire.
Enfin, ce n'est pas la solution la plus simple, je te l'accorde ! C'est juste que j'ai l'impression au final d'y gagner et de rentabiliser le temps que j'ai passé à configurer les différents outils que j'utilise. C'est très subjectif :)
Pour vim + emacs + awesome j'ai tous les fichiers de config. nécessaires pour avoir une expérience agréable en bépo si tu veux, lesquels sont tirés du wiki de bepo.fr.
De plus, changer ses configs c'est l'occasion de personnaliser les raccourcis claviers à son goût. Je l'ai fait rapidement et sans douleur quand je suis passé à bépo, mais c'est du boulot, j'avoue !
Je suis très à cheval sur l'ergonomie et j'ai l'impression que le problème reste grand : on devrait pouvoir choisir tous ses propres raccourcis claviers, de façon modal (type : Ctrl + x + s à la emacs) et de façon centralisée. Mais on en est très très loin !
Un problème supplémentaire que l'on rencontre souvent dans les WM orientés clavier (Awesome, Xmonad et autres), c'est la collision des raccourcis clavier (i.e vim dans tmux dans terminal, dans Awesome, dans X). On se trouve souvent obligés d'associer une touche méta au WM, puis une autre au terminal, et encore une autre à l'éditeur de texte, ce qui réduit considérablement le nombre de raccourcis claviers à proposer.
Mais avec un peu d'astuce on s'en sort ! Par exemple, j'utilise intensivement vim, emacs, tmux, Awesome et Eclipse, le tout avec un agencement bépo, et je ne lève jamais la main du clavier (pas de flèches directionnelles….etc). Le tout avec des raccourcis modaux (pas de Ctrl+Alt+Shift+…). Sisi, c'est possible :)
La méthode B est un exemple des très nombreuses façons de faire de la vérification formelle (encore que B ne fait pas que de la vérification). Il faut aussi regarder toutes les implémentations de model checking, pour ce qui est de la logique temporelle majoritairement, mais aussi les assistants de preuves comme Coq ou encore les outils de comparaison type boite noire, souvent basés sur de la bissimulation, justement pour montrer qu'un programme est bissimilaire à une spécification. Il existe encore d'autres domaines de vérification formelle, donc c'est très très large et cela ne se réduit pas à la méthode B (qui, d'après ce que j'en ai entendu par un de ses concepteurs, a permis de trouver un bug dans le simulateur utilisé pour valider le programme de la ligne 14).
Pour ce qui est de cette histoire de bug sur le karma (pertinent/inutile), je n'ai rien compris, mais si c'est la question, je n'ai jamais cliqué sur le lien « inutile » de quelque commentaire que ce soit :)
C'est un peu la question générale et le thème des réponses apportées. Qu'entends tu par vérification formelle ? Il y a de très nombreuses méthodes, l'aspect difficile étant de modéliser le programme à vérifier et de définir la spécification dans le même formalisme.
Heu… Je ne suis pas 100% sûr de ce que je vais dire, mais il me semble qu'aucun protocole du mail ne chiffre les métadonnées actuellement (adresses, heure d'envois, …etc).
Pour ton histoire de backup, tu peux au moins jeter un œil à rdiff-backup, c'est comme rsync mais en mieux je dirais (j'ai comme toi pour projet d'automatiser proprement mes backups, et je pense que c'est ce que je choisirai).
Au passage, est ce qu'il existe déjà un outils qui ferait tout cela ?
Ben pas vraiment, mais si tu est dans un LAN (disque dur tous branchés sur des machines chez toi), tu peux regarder vers du système de fichiers distribué (à commencer par NFS), tout simplement. Couplé à du rsync (ou rdiff-backup), tu devrais pouvoir sortir un truc simple et puissant.
Pour l'aspect pair-à-pair, il existe des projets comme Tahoe LAFS qui consisteraient à faire du backup communautaire, avec de la redondance et tout et tout. Je ne sais pas si ça correspond à ce que tu recherches, mais tu peux regarder le résumé dans cette dépêche :)
J'ai vu passé des discussions (pas tout suivi dans le détail) là dessus sur les listes crypto-junkies et p2p-hackers (Il y des grosses pointures dessus, mais pas que). Il y a des milliards d'idées et les problèmes ne sont pas simples (notamment vis à vis du spam et de la crypto accessible à tous). Cela dit, j'aime bien l'idée de discuter le problème en profondeur avant de se lancer :)
Mais si jamais je fais quelque chose dans ce sens, ou entend parler d'un truc bien qui se fait, tu le verras passer sur LinuxFr.org :)
[^] # Re: On verra
Posté par vlamy (site web personnel) . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 6. Dernière modification le 28 avril 2014 à 09:35.
Je pense que tu t'égares :)
Que cela soit en distribué ou pas, on a un système que l'on modélise, une spec, un programme et des outils de preuves pour montrer que le programme est conforme à la spec, étant donné le système considéré.
Pour du code, généralement le système est connu : selon le langage tu as un jeu d'instructions, un système de type (c'est encore plus facile à formaliser/prouver, si ton langage a du typage fort), tu peux éventuellement modéliser la mémoire pour certains langages bas niveau et mettre 2/3 contraintes de QoS (puissance CPU, etc.), mais globalement cela s'arrête là.
Pour un système distribué, en plus d'avoir les contraintes d'implémentations, tu as les contraintes de distributions et de sécurité (cf. fautes byzantines), qui ajoutent des problèmes au niveau spécification. De tels problèmes sont connus, il s'agit par exemple de consensus distribué, de synchronisation en environnement asynchrone, d'authentification forte,…etc
Ce sont deux domaines différents, qui ont tous les deux des cas d'usage difficiles à prouver, mais ce que je veux te montrer c'est que si tu apportes de la distribution, tu apportes de la complexité dans le système, donc tout devient plus difficile à commencer par la spécification.
Pour finir :
Avec une modélisation juste d'Internet, c'est-à-dire un système distribué asynchrone dans lequel on ne sait pas distinguer le cas où une machine est lente à répondre ou si elle est en panne, tes propos sont faux. C'est un résultat théorique très connu dans le domaine de l'algorithmique distribué, on le nomme « FLP », pour « Fischer, Lynch, Paterson » et il dit en termes simplifiés :
Ce qui signifie que non : on ne peut pas montrer qu'un consensus se termine ou qu'un système distribué se stabilise, c'est impossible ! Il existe bien entendu des astuces (se reposer sur un serveur centralisé qui fait fois), mais formellement on ne peut pas prouver ce genre de chose si on prend les hypothèses d'un réseau de type WAN.
[^] # Re: On verra
Posté par vlamy (site web personnel) . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 2.
Oui, je t'invite à lire Paxos de Lamport justement, c'est un bon exemple de la complexité qu'un protocole (resp. qu'une spec.) peut avoir.
Attention, je ne dis pas qu'une implémentation est forcément simple, mais des fois (et c'est particulièrement vrai en algorithmique distribuée) la spécification est plus complexe que l'implémentation.
[^] # Re: On verra
Posté par vlamy (site web personnel) . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 9. Dernière modification le 26 avril 2014 à 13:41.
Je confirme que c'est de la fiction, car les productions scientifiques de Lamport et/ou de l'INRIA ne sont pas libres et c'est la guerre entre les labos de recherche. Cela dit, quand l'un a pondu l'article du siècle c'est une avancée qui profite à tous ! D'ailleurs Lamport a déjà bien fait avancer les choses dans le domaine de formalisation des protocoles distribués.
Pour ce qui est de la preuve, attention à ne pas confondre protocole et implémentation ! On peut très bien prouver plein de choses sur les protocoles SSL/TLS, ce qui n'empêchera pas leurs implémentations d'être buggées !
Je veux dire par là que dans la preuve du protocole, on suppose que les méthodes « send(message) » et « receive(message) » sont fiables. Si ce n'est pas le cas (comme pour SSL d'après ce que j'ai compris) la preuve ne tient plus :(
Je me rappelle avoir posé cette question à un chercheur dans le domaine de la vérification formelle : « What if the OS running your proved protocol didn't behave as expected ? Do you run your implementation on proved OS ? Do they run on proved CPU ?»
Sa réponse :
« Fuck ! »
[^] # Re: Solution n°4
Posté par vlamy (site web personnel) . En réponse au journal Héberger son courriel lorsque celui-ci est classé en tant que spam. Évalué à 2.
Je suis aussi tenté par fastmail, mais il y a un point sur lequel je doute : propose t-il aussi des noms de domaine ou serais-je obligé de changer d'adresse pour une adresse en « fastmail.fm » ?
J'ai lu en peu leur page de présentation et j'avoue que je n'arrive pas à me faire une idée clair, il parle de migration facile mais sans parler d'adresse ou de nom de domaine.
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 2.
Y a pas de soucis :)
[^] # Re: Spam et serveur mail
Posté par vlamy (site web personnel) . En réponse au journal Héberger son courriel lorsque celui-ci est classé en tant que spam. Évalué à 2.
Officiellement je n'ai pas acheté du kimsufi, mais l'offre que j'ai y correspond. Il faudrait que je vérifie tout ça, mais je m'y perd dans tous ces noms marketing.
La date de blocage est très récente (< 3 jours) et j'ai ce domaine depuis plus d'un an, donc le problème est autre…
[^] # Re: Spam et serveur mail
Posté par vlamy (site web personnel) . En réponse au journal Héberger son courriel lorsque celui-ci est classé en tant que spam. Évalué à 2. Dernière modification le 24 avril 2014 à 09:34.
Commentaire très intéressant, merci !
J'ai vérifié sur mon nom de domaine (hébergé chez OVH avec le mail associé) et j’apparais dans deux blacklist :
Du coup je suis dubitatif sur cette histoire de nom de domaine qui n'est pas le miens, mais qui fait que j'apparais quand même sur des blacklist.
C'est un problème qui normalement ne devrait pas arriver en auto-hébergement :)
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 4. Dernière modification le 24 avril 2014 à 07:45.
C'est vrai que ce que j'entends par critique c'est le point de vue sécurité (bug = potentielle mort d'homme). Il est vrai que si tu as des contraintes temps réel cela peut changer, mais je n'ai jamais vu de tel code et il me semblait que l'aérospatial misait beaucoup sur Ada pour ce genre de chose notamment.
Sinon tu n'as jamais vu d'Ada ou de Caml ?
[^] # Re: Curiosité
Posté par vlamy (site web personnel) . En réponse au journal Réunion sur IRC pour le projet Bépo. Évalué à 2.
Effectivement, ça donne ça :
[^] # Re: Curiosité
Posté par vlamy (site web personnel) . En réponse au journal Réunion sur IRC pour le projet Bépo. Évalué à 4.
Juste pour éviter les confusions (on est pas vendredi, mais on est quand même sur un sujet pour les déglingos du clavier) :
méta
super (touche Windows)
[^] # Re: Curiosité
Posté par vlamy (site web personnel) . En réponse au journal Réunion sur IRC pour le projet Bépo. Évalué à 3. Dernière modification le 23 avril 2014 à 15:30.
C'est très dommage, car on y gagne vraiment (plus besoin de lever le poignet pour aller chercher les flèches). Et ça représente des kilomètres de parcourus sur une journée.
De toute façon, tant qu'on a pas vraiment essayé, on ne peut pas vraiment se rendre compte (c'est comme le bépo).
Bref, ce qu'il te faut c'est jouer à vim adventures
PS: bon le truc con c'est que c'est un mapping azerty/qwerty pour le jeux, mais si c'est juste pour « jklm », tu peux repasser en azerty juste pour le jeux et ensuite switcher dans vim sur « ctsr » :)
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 2.
Non je ne connais pas de tuto, malheureusement.
Par contre, ce qui est sûr, c'est que tous les gens que j'ai vu coder sur des trucs critiques n'utilisaient pas C, ou alors via des générateurs de code, comme c'est le cas notamment dans certaines branches de l'aéronautique.
[^] # Re: Curiosité
Posté par vlamy (site web personnel) . En réponse au journal Réunion sur IRC pour le projet Bépo. Évalué à 2. Dernière modification le 23 avril 2014 à 14:22.
Je suis d'accord cela ne convient pas à tous les postes. Je suis développeur et j'édite tout sur ma machine, y compris tout ce que je peux accéder via ssh (config sur serveurs, …etc). Je n'ai donc aucun problème de remapage, mais j'imagine que ce n'est pas le cas de tout le monde.
Quant aux machines des collègues, non je ne les remappe pas (je ne vois pas bien pourquoi je le ferais au passage). J'ai juste un clavier azerty pas loin à brancher sur ma machine en cas de besoin, et ça fait généralement l'affaire.
Enfin, ce n'est pas la solution la plus simple, je te l'accorde ! C'est juste que j'ai l'impression au final d'y gagner et de rentabiliser le temps que j'ai passé à configurer les différents outils que j'utilise. C'est très subjectif :)
[^] # Re: Curiosité
Posté par vlamy (site web personnel) . En réponse au journal Réunion sur IRC pour le projet Bépo. Évalué à 3.
Parce que sur IRC il n'y a ni bière, ni vin, ni victuailles en tout genre !
[^] # Re: Curiosité
Posté par vlamy (site web personnel) . En réponse au journal Réunion sur IRC pour le projet Bépo. Évalué à 3.
Pour vim + emacs + awesome j'ai tous les fichiers de config. nécessaires pour avoir une expérience agréable en bépo si tu veux, lesquels sont tirés du wiki de bepo.fr.
De plus, changer ses configs c'est l'occasion de personnaliser les raccourcis claviers à son goût. Je l'ai fait rapidement et sans douleur quand je suis passé à bépo, mais c'est du boulot, j'avoue !
Je suis très à cheval sur l'ergonomie et j'ai l'impression que le problème reste grand : on devrait pouvoir choisir tous ses propres raccourcis claviers, de façon modal (type : Ctrl + x + s à la emacs) et de façon centralisée. Mais on en est très très loin !
Un problème supplémentaire que l'on rencontre souvent dans les WM orientés clavier (Awesome, Xmonad et autres), c'est la collision des raccourcis clavier (i.e vim dans tmux dans terminal, dans Awesome, dans X). On se trouve souvent obligés d'associer une touche méta au WM, puis une autre au terminal, et encore une autre à l'éditeur de texte, ce qui réduit considérablement le nombre de raccourcis claviers à proposer.
Mais avec un peu d'astuce on s'en sort ! Par exemple, j'utilise intensivement vim, emacs, tmux, Awesome et Eclipse, le tout avec un agencement bépo, et je ne lève jamais la main du clavier (pas de flèches directionnelles….etc). Le tout avec des raccourcis modaux (pas de Ctrl+Alt+Shift+…). Sisi, c'est possible :)
[^] # Re: Github
Posté par vlamy (site web personnel) . En réponse à la dépêche Redmine Git Hosting 0.7. Évalué à 3.
Peut être pour bénéficier de l'aspect réseau social de github ? Ce qui, soyons honnêtes, devrait aider à le faire connaître.
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 2. Dernière modification le 18 avril 2014 à 14:51.
La méthode B est un exemple des très nombreuses façons de faire de la vérification formelle (encore que B ne fait pas que de la vérification). Il faut aussi regarder toutes les implémentations de model checking, pour ce qui est de la logique temporelle majoritairement, mais aussi les assistants de preuves comme Coq ou encore les outils de comparaison type boite noire, souvent basés sur de la bissimulation, justement pour montrer qu'un programme est bissimilaire à une spécification. Il existe encore d'autres domaines de vérification formelle, donc c'est très très large et cela ne se réduit pas à la méthode B (qui, d'après ce que j'en ai entendu par un de ses concepteurs, a permis de trouver un bug dans le simulateur utilisé pour valider le programme de la ligne 14).
Pour ce qui est de cette histoire de bug sur le karma (pertinent/inutile), je n'ai rien compris, mais si c'est la question, je n'ai jamais cliqué sur le lien « inutile » de quelque commentaire que ce soit :)
[^] # Re: Vérification formelle
Posté par vlamy (site web personnel) . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 4.
C'est un peu la question générale et le thème des réponses apportées. Qu'entends tu par vérification formelle ? Il y a de très nombreuses méthodes, l'aspect difficile étant de modéliser le programme à vérifier et de définir la spécification dans le même formalisme.
# Coccinelle
Posté par vlamy (site web personnel) . En réponse au journal Idée stupide sur la sécurité du code. Évalué à 7.
Il y a Coccinelle aussi, qui est orienté C et est utilisé, notamment, sur le kernel Linux. Il paraît que c'est pas mal et en plus c'est Français :)
[^] # Re: Une news en attente
Posté par vlamy (site web personnel) . En réponse au journal Sortie de shinken 2.0. Évalué à 5.
Effectivement, vu le niveau du journal, la concurrence n'est pas très rude.
Tiens, je ne suis pas le lien et j'attends la dépêche, pour la peine !
[^] # Re: Mail dépassé
Posté par vlamy (site web personnel) . En réponse au journal Thunderbird : j'en peux plus ! Qui arrive à l'utiliser pour de vrai ? Quoi d'autre ?. Évalué à 1.
Heu… Je ne suis pas 100% sûr de ce que je vais dire, mais il me semble qu'aucun protocole du mail ne chiffre les métadonnées actuellement (adresses, heure d'envois, …etc).
[^] # Re: Clarté ?
Posté par vlamy (site web personnel) . En réponse au journal index2share v0.5.72 “indexer, choisir et copier des fichiers” . Évalué à 2.
Ça à l'air bon ça, faut que jette un œil :)
[^] # Re: Clarté ?
Posté par vlamy (site web personnel) . En réponse au journal index2share v0.5.72 “indexer, choisir et copier des fichiers” . Évalué à 2.
J'essaie de répondre rapidement :)
Pour ton histoire de backup, tu peux au moins jeter un œil à rdiff-backup, c'est comme rsync mais en mieux je dirais (j'ai comme toi pour projet d'automatiser proprement mes backups, et je pense que c'est ce que je choisirai).
Ben pas vraiment, mais si tu est dans un LAN (disque dur tous branchés sur des machines chez toi), tu peux regarder vers du système de fichiers distribué (à commencer par NFS), tout simplement. Couplé à du rsync (ou rdiff-backup), tu devrais pouvoir sortir un truc simple et puissant.
Pour l'aspect pair-à-pair, il existe des projets comme Tahoe LAFS qui consisteraient à faire du backup communautaire, avec de la redondance et tout et tout. Je ne sais pas si ça correspond à ce que tu recherches, mais tu peux regarder le résumé dans cette dépêche :)
[^] # Re: Clarté ?
Posté par vlamy (site web personnel) . En réponse au journal index2share v0.5.72 “indexer, choisir et copier des fichiers” . Évalué à 2.
Et donc, où veux tu en venir robin ?
Si on travaille sur une API ou un wrapper tu aurais un langage de prédilection ?
[^] # Re: Mail dépassé
Posté par vlamy (site web personnel) . En réponse au journal Thunderbird : j'en peux plus ! Qui arrive à l'utiliser pour de vrai ? Quoi d'autre ?. Évalué à 2.
Ouais enfin on n'y est pas encore !
J'ai vu passé des discussions (pas tout suivi dans le détail) là dessus sur les listes crypto-junkies et p2p-hackers (Il y des grosses pointures dessus, mais pas que). Il y a des milliards d'idées et les problèmes ne sont pas simples (notamment vis à vis du spam et de la crypto accessible à tous). Cela dit, j'aime bien l'idée de discuter le problème en profondeur avant de se lancer :)
Mais si jamais je fais quelque chose dans ce sens, ou entend parler d'un truc bien qui se fait, tu le verras passer sur LinuxFr.org :)