La 2CV présente pourtant une qualité essentielle que n'a pas la C1: tu n'as pas besoin de te battre contre pour la réparer sans passer par un garage qui dispose d'une valise électronique.
Hum, et elle a un défaut essentiel : si tu n'as pas les compétences pour la réparer toi même, c'est la croix et la bannière pour trouver un garagiste compétent.
rugby est un ancien mot basque pour dire « je fais 1m90 et peut broyer des briques entre mes mains nues mais ai toujours mon complexe d'infériorité par rapport aux footballeurs »
NdM : rien ne change du côté du contrôle total de l'AppStore... à moins que l'utilisateur ne s'en sorte avec l'interdit jailbreak (ne manque dans les annonces que l'iMembête...).
Il y a qques jours DropBox est entré dans Debian. Ma première réaction a été de dire « c'est génial ce truc ! », ma deuxième de dire « et la confidentialité la dedans ? » et enfin « mais puisque je m'auto héberge, pourquoi ne pas le faire moi même ?»
Dropbox takes the security and privacy of your files very seriously.
[...]
* All transmission of file data and metadata occurs over an encrypted channel (SSL).
* All files stored on Dropbox servers are encrypted (AES-256) and are inaccessible without your account password.
[...]
* Dropbox employees are not able to view any user's files.
En réalité il s'agit des instructions SSSE3 comme indiqué dans le journal antérieur à la dépêche, et la liste des processeurs supportant ces dernières est tout de suite plus mince :http://en.wikipedia.org/wiki/SSSE3
Le fait que coq soit - si je ne m'abuse - vérifié par lui-même est un gros plus et j'ai plus confiance en lui pour cela que pour le fait qu'il soit vérifié par X personnes.
Tu t'abuses : Coq n'est pas vérifié lui-même, et c'est impossible par application du second théorème d'incomplétude.
N.B. : Je ne parle que des assistants à la preuve (surtout ceux basés sur le principe de de Bruijn pour les connaisseurs).
Une preuve en math à la main peut être vérifiée, si longue soit-elle. C'est d'ailleurs ce qui s''est passé avec la preuve du théorème de Fermat. A partir du moment ou tu confies la vérification à la machine, il faut:
- avoir confiance dans le programme (ou le vérifier).
J'ai plus confiance en un programme simple (< 10 kloc) et unique vérifié par des dizaines d'experts qu'en un humain, fut-il mathématicien. D'autant plus que toutes les preuves ne bénéficient pas de l'attention soutenue d'un comité de génies ; passons aimablement sur les lemmes « triviaux donc laissés à la charge du lecteur », facilité dont un ordinateur ne se satisfera que très partiellement. Est-ce grave ? Franchement, je ne le pense pas. Je m'élève juste contre des affirmations à l'emporte-pièce qui mélangent un peu preuve par ordinateur et cuisine numérique tendance empirisme-vaudou.
C'est l'idée de faire vérifier à un ordinateur qui est sale.
Et pourquoi donc ?
Je crois qu'il y a une confusion entre une preuve formelle en Coq, plus sûre qu'une preuve de maths à la main (et plus dure à produire, no free beer) et une « preuve » comme celle de 1976 pour le théorème des quatre couleurs où on a basiquement un gros programme Fortran qui calcule deux semaines et finit par répondre « OUI » ou « NON ».
YARV et Rubinius semble partager l'objectif d'être une implantation performante de Ruby via une VM « native » (à l'inverse de JRuby), mais YARV est le futur Ruby « officiel », béni par Matz. Un rapprochement des deux serait-il possible en théorie, ou quelque-chose m'échappe dans les buts fondamentaux des deux projets ?
Par curiosité, où vois-tu du Mandriva à Paris 6 :-o ? À ce que je sache l'écrasante majorité des postes de salles de TP est sous double-boot Scientific Linux / Windows (2000 ?).
[^] # Re: Je trouve ça affligeant
Posté par auve . En réponse au journal Mon téléphone est mort, vive mon (nouveau) téléphone. Évalué à 4.
[^] # Re: As tu pensé à l'economie ?
Posté par auve . En réponse au journal Defective By Design, ou le business model des bugs volontaires.. Évalué à 4.
Hum, et elle a un défaut essentiel : si tu n'as pas les compétences pour la réparer toi même, c'est la croix et la bannière pour trouver un garagiste compétent.
[^] # Re: Dispensable
Posté par auve . En réponse à la dépêche Aficionados de la console, Google pense à vous et sort Google CL tools. Évalué à 7.
[^] # Re: Et alors quel est le rapport avec le Libre?
Posté par auve . En réponse au journal La coupe du monde. Évalué à 10.
[^] # Re: Et alors quel est le rapport avec le Libre?
Posté par auve . En réponse au journal La coupe du monde. Évalué à 2.
[^] # Re: resolution de l'oeil
Posté par auve . En réponse à la dépêche Quoi de neuf chez Apple ?. Évalué à 4.
ou pas, la situation s'améliore un peu coté scripting embarqué dans l'appli : http://www.appleinsider.com/articles/10/06/11/apple_relaxes_(...)
[^] # Re: C'est drôle !
Posté par auve . En réponse à la dépêche SparkleShare pour partager vos fichiers sur internet. Évalué à 1.
Dropbox takes the security and privacy of your files very seriously.
[...]
* All transmission of file data and metadata occurs over an encrypted channel (SSL).
* All files stored on Dropbox servers are encrypted (AES-256) and are inaccessible without your account password.
[...]
* Dropbox employees are not able to view any user's files.
Source : http://www.dropbox.com/features
On pourra toujours me rétorquer que, le démon n'étant pas libre, il est difficile de vérifier la véracité de ces dires.
[^] # Re: Pour durer longtemps…
Posté par auve . En réponse au journal Ordinateur portable = Ordinateur jetable. Évalué à 2.
[^] # Re: Pour durer longtemps…
Posté par auve . En réponse au journal Ordinateur portable = Ordinateur jetable. Évalué à 8.
L'écran brillant est maléfique, il abîme ton PC, bat ta femme, met tes enfants sur le trottoir et vote UMP !
[^] # Re: Bah, c'est du bon sens
Posté par auve . En réponse au journal Google interdit l'usage de windows à ses employés. Évalué à 3.
[^] # Re: Commentaire
Posté par auve . En réponse au journal Galaxy Zoo - il revient et il est très content. Évalué à 4.
[^] # Re: Commentaire
Posté par auve . En réponse au journal Galaxy Zoo - il revient et il est très content. Évalué à 8.
[^] # Re: Krita != Gimp
Posté par auve . En réponse à la dépêche KOffice 2.2 est sorti. Évalué à 5.
[^] # Re: ça va déboiter!
Posté par auve . En réponse à la dépêche Sortie de MeeGo 1.0. Évalué à 10.
[^] # Re: ça sert quand même à faire des bombes…
Posté par auve . En réponse au journal Un français #3 dans le Top500. Évalué à 7.
[^] # Re: En souvenir de son infirmation de la conjecture des quatre couleurs.
Posté par auve . En réponse au journal Martin Gardner (1914-2010). Évalué à 3.
Tu t'abuses : Coq n'est pas vérifié lui-même, et c'est impossible par application du second théorème d'incomplétude.
[^] # Re: En souvenir de son infirmation de la conjecture des quatre couleurs.
Posté par auve . En réponse au journal Martin Gardner (1914-2010). Évalué à 3.
Une preuve en math à la main peut être vérifiée, si longue soit-elle. C'est d'ailleurs ce qui s''est passé avec la preuve du théorème de Fermat. A partir du moment ou tu confies la vérification à la machine, il faut:
- avoir confiance dans le programme (ou le vérifier).
J'ai plus confiance en un programme simple (< 10 kloc) et unique vérifié par des dizaines d'experts qu'en un humain, fut-il mathématicien. D'autant plus que toutes les preuves ne bénéficient pas de l'attention soutenue d'un comité de génies ; passons aimablement sur les lemmes « triviaux donc laissés à la charge du lecteur », facilité dont un ordinateur ne se satisfera que très partiellement. Est-ce grave ? Franchement, je ne le pense pas. Je m'élève juste contre des affirmations à l'emporte-pièce qui mélangent un peu preuve par ordinateur et cuisine numérique tendance empirisme-vaudou.
Un peu de lecture : http://coq.inria.fr/faq?som=2#htoc7
- avoir confiance dans les données qu'il reçoit (ou les vérifier).
Quelles données ? Du moment que le théorème est bien écrit, tu n'as justement pas à vérifier la preuve, et c'est tout le principe.
[^] # Re: En souvenir de son infirmation de la conjecture des quatre couleurs.
Posté par auve . En réponse au journal Martin Gardner (1914-2010). Évalué à 3.
Et pourquoi donc ?
Je crois qu'il y a une confusion entre une preuve formelle en Coq, plus sûre qu'une preuve de maths à la main (et plus dure à produire, no free beer) et une « preuve » comme celle de 1976 pour le théorème des quatre couleurs où on a basiquement un gros programme Fortran qui calcule deux semaines et finit par répondre « OUI » ou « NON ».
# Question de béotien
Posté par auve . En réponse à la dépêche Rubinius 1.0 est sorti. Évalué à 10.
[^] # Re: TL;DR
Posté par auve . En réponse au journal QML: le futur des interfaces graphiques. Évalué à 2.
[^] # Re: Gros ratage.
Posté par auve . En réponse au journal De l'abération de la notion même d'antivirus. Évalué à 5.
[^] # Re: Installinging software was never this easy and powerful !
Posté par auve . En réponse au journal Brainstorming : ce que Linux a de mieux que mac os. Évalué à 5.
2/ Quel est le comble pour un Linuxien ? Demander l'intérêt de la solution N+1.
[^] # Re: Nouvelles fonctionnalités
Posté par auve . En réponse à la dépêche Emacs, brevets, et Ubuntu Unity et Light. Évalué à 3.
CEDET est censé faire ce genre de chose. Je n'avais jamais réussi à le faire marcher à l'époque où je cherchais ce genre de choses.
Est-il possible de sauter sur la définition d'un terme C ?
Euh, find-tag + exuberant ctags devrait faire ce que tu veux.
Est-il possible de faire lister les sites d'appel d'une fonction ?
cscope.el ?
[^] # Re: On ne vous prend pas pour des cons !
Posté par auve . En réponse au journal Brainstorming : ce que Linux a de mieux que mac os. Évalué à 3.
[^] # Re: l'ambEUlance
Posté par auve . En réponse au journal Linux : Mandriva à vendre. Évalué à 1.