lambada a écrit 42 commentaires

Encore faudrait-il être confiant dans le fait que le prouveur Coq est plus stable que la JVM...

Si stable = exempt de bugs ici, alors pour faire confiance à une preuve écrite par Coq tu dois faire confiance au coeur de Coq, relativement petit justement pour éviter les risques (+ le hardware, le compilo et autres cités plus haut mais ça s'applique aussi à la JVM).

que la probabilité d'erreur dans les preuves humaines qui se cache derrière soit plus faible que la probabilité d'erreur dans le code de la JVM.

Si la preuve passe Coq, elle est garantie sans erreur et le code généré aussi, c'est bien l'intérêt.
(bien sur en partant des principes donnés plus haut concernant le coeur de coq, le compilo, la génération de code, la théorie et autres)
http://coq.inria.fr/doc/faq.html#htoc7

On tombe dans un problème d'oeuf et de poule c'est comique.

Le problème c'est qu'on ne puisse pas réécrire Coq en Coq, mais bon ! Sacré Kurt ;-)

Etant donné le nombre de personnes qui utilise Coq et le nombre de personnes qui utilisent la JVM, je suis plus que réservé...

De toute façon j'apportais juste des précisions sur le fonctionnement de Coq, pas de son applicabilité à l'écriture d'une VM. Xavier Leroy et son équipe semblent s'intéresser à l'écriture d'un compilo prouvé formellement :
http://pauillac.inria.fr/~xleroy/compcert-backend/
http://pauillac.inria.fr/~xleroy/publi/cfront.pdf
http://groups.google.com/group/fa.caml/browse_thread/thread/(...)

Finalement on le sait, on peut poster à travers un trou noir \o/

Je ne connais pas B, mais je sais qu'en Coq, tu écris ta spécification dans un langage particulier, puis la prouves interactivement, avec certaines étapes plus ou moins automatisées à l'aide de "tactiques", plusieurs bibliothèques de ces dernières étant disponibles.

Une fois la preuve établie (c'est évidemment la partie difficile), Coq est capable d'en extraire un code source en OCaml ou Haskell (via l'isomorphisme de Curry-Howard) qui sera correct par construction (si tant est que le petit coeur "trusted" de Coq, les axiomes, le compilo OCaml, le hardware, l'OS soient eux-mêmes dignes de confiance bien sur).

Coq ne part pas d'un programme pré-existant pour essayer de prouver sa correction vis à vis des spécifications.

Roooh et [ ] Pierre Tramo ? C'est le sondage ou jamais !

Il semblerait que http://les.saimal.saimal.fr

Hmmm, c'est sur que la clé censée rester secrète sorte de la TPM ?

NON ! Je ne peux pas te laisser dire ça. Le C est beau, le C est grand. Qui n'a jamais été émoustillé par la majesté d'une suite de #ifdef imbriqués ou par une erreur de segmentation... Ces moments émouvants qui rappellent au programmeur qu'il doit rester humble face à la machine.

Devoir réécrire une implémentation des structures de base à chaque programme, écrire avec amour son Makefile récursif ou ses graciles macros M4, voilà des bonheurs simples qui forment la vie passionante d'un dev C. Au diable la glib !

La supériorité des outils C est incontestable, comme en témoigne le foisonnement d'IDE libres de grande qualité pour ce langage. D'ailleurs, y a-t-il un équivalent de Valgrind pour détecter les erreurs de pointeurs en Java et C# ? Je vous laisse deviner : même pas. Ah c'est sur pour implémenter une AbstractProtocolSingletonFactory y a du monde, mais pour le reste...

Que les Monomaniaques de l'UML avec Objecteering tremblent, les codeurs C n'ont à perdre que leurs chaînes de compilation ! Les Javaistes & co seront rééduqués, tout comme les Lispeux et les Smalltalkiens en leurs temps !

À la rigueur, les gens voulant faire de l'objet peuvent se tourner vers un langage simple et conceptuellement élégant, le C++.

Carl "Mad" Marx

Je vois que les moinsseurs sophistes s'en donnent à coeur joie sur mon ami Ned< !

Je vais donc démontrer l'inanité de cette chose barbare qui est aux encodages ce qu'une statue du Pape est à l'Art.

wmCoinCoin est parfait. Il a donc toutes les qualités. Or il ne gère pas l'UTF-8. Donc l'UTF-8 n'est pas une qualité. Gérer toutes les features possibles et imaginables du moment qu'elles ne sont pas des défauts (y compris les features "neutres" dont on pourrait se passer) est une qualité. L'UTF-8 n'étant ni bonne, ni neutre, c'est une mauvaise feature !

Dans ce contexte, il est donc évident que l'UTF-8 est l'oeuvre d'une association communisto-libérale de fabricants de RAM¹ pour s'assurer des profits substantiels dans les années à venir. Des travaux récents ont même remis en question l'existence de la Chine qui sert d'alibi à la cabale (qui selon certains autres travaux n'existerait pas).

C'est la faute de ces gens si de nos jours on s'éloigne du C, qui est le langage le plus beau, puissant et élégant de tous ceux qui existent ! Est-ce que vous avez besoin d'un GC ? D'exceptions ? D'un vrai systèmes de type ? D'une bibliothèque standard utilisable pour autre chose qu'un hello world ?

Messieurs les moinsseurs, je ne vous salue pas !

¹ : http://sam.zoy.org/writings/utf8/

C'est pas RMS, le pape à geek ? /o\

/ddos jabber.org</Gniarf>

http://faisun.blog.com/

Fred Coppula !

d'ailleurs faudrait un chan IRC pour se tapper sur la geule à coup de troll...

Mais ça existe déjà, c'est #linuxfr sur FreeNode !

(Ce post est dédicacé à Gniarf)

>Linux va peut-être pouvoir récupérer directement le code du ZFS
>original issu de Solaris !

Ouais, à la lecture du blog zfs-on-fuse il est clair qu'il suffira de changer quelques #IFDEF pour passer du VFS de Solaris à celui de Linux ;-)

peacemaker

Assassin ! (Sorbonne, zéro ! /o\)

à part MS. (pardon)

Tu connais Smalltalk ? Self¹ ? Io² ?

¹ : http://research.sun.com/self/language.html

² : http://iolanguage.com/

C'est pour que d'autres personnes ne repompent pas le design.

===>[]

Mea culpa, j'ai confondu la conception virginale (le cas qui nous intéresse) et l'immaculée conception (celle de Marie donc, bien postérieure à la Bible). C'est décidément très compliqué les histoires de cul en religion.

marie est tombee enceinte sans se prendre sa riflee

Ça c'est pas dans la Bible à ma connaissance.

J'aime bien Linus, mais de là à le mettre aux cotés de Mandela ou autres... RMS à la rigueur.

"Chaque méthode est traditionnellement munie de méthodes" ?

s/méthode/objet/ ?

Tais toi boulet, tu vas nous attirer des ennuis !

Un fabricant de graveurs.

===>[]

>Un peu comme si quelqu'un faisait une VM pour executer du code
>c++ compile...

http://llvm.org ?

(compilé certes mais pas en natif, plus toute les possibilités d'optimisations à l'exécution)

Euh, c'est pas comparable. Théoriquement (je ne suis pas juriste), tout le code qui lie avec du code GPL doit lui même être GPL.
Pour répondre au commentaire un cran plus haut, il me semble que la GPL de Linux a une clause spéciale pour autoriser l'exécution de programmes propriétaires.