Il se trouve que dans le monde des langages a objet, tu ne trouvera pas de système d'exploitation. Et très peu de bibliothèque (performante) bas niveau.
Car justement le résultat de la compilation n'est pas terrible en prog objet.
Et l'interet du modèle prototype de lisaac est qu'il permet de mettre en place des techniques de compilation plus efficace pasque le langage s'y prete bien.
Oui mais c'est un problème de communication de la platforme du langage avec le reste de la machine pas du langage en soit. Enfin je suis d'accord avec ce que tu dis.
Je sais bien que c'est ce que fait gtk et personnellement je n'échangerai pas deux barils de gtk contre un baril de qt.
Alors après il y a d'autre avantage a l'utilisation de gtk : binding plus facile avec d'autre langage, compilo plus performant que celui de c++.
Mais justement si on arrive à résoudre ces problèmes je preferai largement programmer en objet.
Évidement le traitement a réaliser est le même. et oui cela a déjà été fait.
Ouais mais aucun compilateur ne permet d'utiliser toutes les techniques objet pour du code dont la rapiditée d'exécution est critique. Genre dans ce genre de biblio
Par exemple si tu regarde les autres projets (y'a des liens sur le site de lisaac) de codage d'un os avec un langage objet ils recommandent tous de ne surtout pas utiliser le polymorphisme. du coup on ne voit pas trop l'interet d'utiliser un langage objet. Alors qu'ici le but est bien de ne pas se restreindre et de garder l'efficacitée.
En ce moment c'est a la mode de dire que les concept objet c'est juste une vision de l'esprit et que l'on peut faire de l'objet avec n'importe quel objet.
Alors c'est vrai oui, de la même facon que l'on peut tout réaliser avec n'importe quel langage, ils sont tous turing-complet.
Mais il y aussi indéniable que si on utilise des langages bien adapté a ce que l'on veut faire on arrive plus vite a un meilleur résultat.
Perso je pense que refaire le travail du compilateur tous les jours pasque on essaie de faire de l'objet avec du C, ben c'est une mauvaise idée.
Alors évidement il faut absolument un compilo qui tienne la route, ce qui est le cas ici.
Non effectivement je ne fais plus de ML. Mais j'ai déjà lu les livres que tu cite.
D'un autre coté je me souviens pas d'avoir été aussi agressif avec toi !
Cette syntaxe est effectivement tres naturelle.
Mais ceci n'est pas une definition du for mais une utilisation du for comme définie dans la grammaire de caml. Donc ca n'a rien a voir avec mon discours.
Et il se repose compltement sur gcc puisque il génére du C avec quelques extension de gcc.
Et quand je disais que c'était comme dans Lisaac, c'est parcque les templates sont réellement des citoyen de premiere classe et que le compilo est déjà efficace.
Et la syntaxe et la sémantique de C++ ne permettront jamais d'avoir un compilo qui génére du code aussi performant que celui de lisaac. t'aura beau mettre 400 personnes dans le projet g++ ca ira pas
Parceque justement un bon paquet d'optimisation automatique dans lisaac sont prévue pour être fait à la main en C++. Et que le langage est trop complexe
Mais concernant le troll, je pense qu'au contraire la prochaine fois que j'écrit un journal je vais en inclure 2-3 dedans :) . Regarde, sans le troll sur Ocaml on aurait jamais eu ton commentaire ! Ici ca marche au troll...
Il me semble que C++0x devrait resoudre la plupart de tes griefs a l'encontre des templates[*].
Cela se resume a: "make templates a first class citizen".
[*] encore faut-il que les compilos suivent derriere, je le concede volontiers.
Évidement ca ne change rien au fait que sorti des fonction de base comme drawLine le travail reste compliqué. (je dis ca avant que quelqu'un d'autre le dise :))
Oui c'est vrai mais bon ca reste qd même du ML avec en bonus l'impératif et l'objet.
D'un point de vue syntaxe et sémantique on marie des choses par la force. Et au final on se retrouve avec un langage tres tres gros (ML + impératif + classe + module). Perso j'aurai préféré qu'ils gardent la simplicité du langague d'origine, bon ce n'était pas forcement possible
C'est tout a fait l'opposé de la philosophie de lisaac. cf la grammaire http://isaacos.loria.fr/li_docs.html qui est très courte mais le langage reste quand même tres expressif.
Par exemple voici la définition de la boucle for. En fait c'est très proche d'un itérateur sur les entier tel que l'on aurait pus le définir en Caml.
to limit_up:SELF do blc:BLOCK <-
(
(self<=limit_up).if {
blc.value self;
(self+1).to limit_up do blc;
};
);
en caml (pas objet) ca aurait fait un truc du style
let rec for i limit_up blc=
if i<limit_up
then blc i;for (i+1) blc
else blc i
;;
du type int -> int -> (int -> ()) ->() (a vue de nez)
(mon caml est rouillé donc ca doit être faux, mais j'ai pas envie d'installer le compilo)
Je trouve que c'est un exemple très réussit d'intégration de concept plutot fonctionnel à l'intérieur d'un langage objet mais sans rajouter des construction plus ou moins étrangère dans la syntaxe de base. En fait ce qu'il ont eu besoin de rajouter c'est le type BLOCK correspondant a un suite d'instruction séquentielles. Comme ca on peut passer des blocs a itérer au la commande for (enfin to do : on peut définir plusieur mot clef).
Oh ben non, c'est pas trop dur : suffit d'hériter...
J'aurai du préciser pas trop dur par rapport a l'avancé du projet (il me semble qu'un portage sur ARM a déjà été fait) et a la difficulité des techniques habituelles.
Apres évidement je pense que tout le monde a une idée de la quantité de travail derrière ...
J'imagine qu'il faudrait adapter le compilo avec une bibliothèque spéciale représentant les capacités des shaders. et compiler differement le code selon que cela fait partie de d'appli utilisatrice ou des shader a destination de la carte.
Par contre le compilo lisaac est prévu pour faire du c, donc faudrait en prime refaire tous la partie arrière pour sortir l'asm des shaders.
C'est vrai que cela serait intéressant de voir si le modèle proposé resiste au choc.
Mais les shader ca ce programme pas indépendament du logiciel qui l'utilise avec un espece d'assembleur standard ? j'ai pas l'impression que les shaders ca fait partie du driver mais je suis pas un spécialiste
Pour le moment on a juste le compilo dans un fichier c généré depuis la version en lisaac. Et isaac (l'os) dans un fichier c aussi généré depuis la version en lisaac. Par contre la lib est dispo en lisaac. (le tout en licence cecill)
Mais ils ont l'air assez ouvert au libre maintenant. Alors je pense qu'il faut mettre la pression jusqu'a ce que ils fournissent le compilo (surtout) et l'os. Histoire qu'ils sentent qu'on est derrière et qu'on est intéressé d'en faire un projet libre.
Pour répondre à ta question techniquement je pense pas que cela soit trop dur, c'est quoi dans un iPaq un ARM ?
Faire un driver c'est simple. Faire un driver efficace et qui tire partie des atouts du matos, c'est une autre pair de manche, et c''est pas trop le langage qui fait la différence, mais la façon dont intéragit le matos avec le driver.
Je ne suis pas d'accord c'est plus facile de *bien* faire intéragir le matos avec le driver si on a un langage qui permet d'exprimer plus facilement ce que l'on essaye de faire.
Evidement ca ne change rien de fondamental (rien non plus aux problemes de spec non disponible), mais je pense que la rédaction de driver serai plus rapide de plusieurs ordres de grandeur si on abandonne le C pour un langage plus haut niveau.
Lisaac (avec deux a) est beaucoup plus jeune que Ocaml.
Ca ne fait que très recement qu'il y a une version utilisable de Lisaac. En plus le développement a été réalisé par une seule personne (+un ingé pendant 2 ans).
On est au tout début pour Lisaac alors que Ocaml a déjà une longue histoire et est mature.
Perso je trouve que Caml a un bon succes ...pour un langage fonctionel, je ne pense pas qu'on puisse attendre beaucoup plus.
Alors que Lisaac est impératif objet et bien adapté pour faire des choses efficaces.
Quand au C/C++, tu juges ça inommable, mais c'est eux qui composent 95% des gros programmes, et ce n'est pas pour rien.
C'est de moins en moins vrai, pour les appli utilisateur desktop oui mais en entreprise ca a beaucoup évolué vers Java. Et cela évoluera encore, c lent mais ca bouge qd même
Quand je vois que le Caml, prétendumment très à l'aise avec le typage, pas foutu de faire la différence entre un entier et un flottant si on ne rajoute pas un point à l'opérateur, ça me fait plus pitié qu'autre chose...
mdr, c'est sur que faire la différence entre (je veux un entier) 3+4 et (je veux un flottant) 3+4 c'est réalisé par tout les compilo du monde.
C'est exactement pareil pour tout les langage a un moment donné il faut que tu dise au compilo quel type tu veux utiliser. Or il n'y a pas de déclaration de type en Caml donc ils utilisent des opérateur différent "+" et "+.". Dans le contexte c'est la seul manière de faire.
Apparement tu a encore des progres a faire en prog fonctionnelle :)
Sérieusement ce qui est vraiment dommage c'est qu'ils n'ont pas utilisé l'extension objet de OCaml pour définir un type Nombre et uniffier l'interface des opérateurs entre les entiers et les flottants.
Pour en revenir au sujet : ce point la est traité correctement en Lisaac. On manipule les différentes type de nombres (entiers ...) suivant la même interface.
C'est intéressant car parmi les critiques relevées par l'articles il y a
dynamic type systems (...) correctness, safety, predictability and efficiency
.
Mais lisaac est typé statiquement et compilé, il est donc plutot sur et efficace. Donc il répond à la plupart des critiques.
A part la dernière sur le fait que les developpeur ne sont pas familier avec cette technique. Mais bon ca c'est comme n'importe quel innovation. Genre y'a plein de gens qui sont boulonné au C et qui ne veulent surtout pas changer, quelque soit les arguments qu'on leur donne. A mon avis c'est le peur de quitter un environnement familier où ils exercent un position privilégiée ... surtout quand la nouvelle technique rend caduque un travail autrefois fait à la main !
Au contraire on peut surcharger les méthodes du driver generique logiciel par celle fournie par le materiel. Par exemple pour remplacer l'affichage logiciel d'un bitmap qui utilise set_pixel par une methode qui réalise l'appel a la carte graphique.
Et puis ce qu'il faut voir c'est que la plupart des méthode formelles ne sont jamais sortie des labo de recherches.
Et il en existe un sacré paquet pourtant des méthodes ...
alors je considere ca normal d'utiliser tjrs cet exemple et d'en être fier surtout que c'est une étape fondamentale dans l'histoire du B.
Et celui ci a évolué depuis. On est passé au B événementiel et une nouvelle version des outils est en préparation http://rodin-b-sharp.sourceforge.net/ en plus cela sera libre.
Plein de cas courant peuvent être résulu, et c'est cela qui nous permet d'écrire des prouveurs, ou de faire marcher des algos de model-checking.
Il n'empeche que même dans les cas courant (de l'industrie) il y a des cas emmerdant qui ne fonctionnent pas avec les techniques actuels. Que cela soit avec le prouveur de B ou n'importe quel autre. La principale limite étant que la complexité de ce genre d'algo est généralement exponentielle. Alors qu'un être humain arrive, plus ou moins, a *voir* la solution directement.
En pratique en B on dirige le prouveur en lui faisant faire des cas intermédiaire et en lui machant le travail. Alors même dans les preuve à la main le prouveur est essentiel.
Perso je trouve que ca marche pas trop mal, bon ok defois on s'arrache les cheveux et sa demande pas mal d'expérience et de temps.
C'est même le seul exemple. On me le donnait déjà en 2000.
Et alors ?
Si c'est une réthorique de ta part pour sous-entrendre que le B n'a jamais servis a rien d'autre, je trouve ca mesquin. Je ne vais pas chercher d'autre exemples pour te faire plaisir.
Et encore, les mauvaises langues disaient que la pluspart des preuves avaient été faite à la main.
Je n'ai prétendu que toute les preuves avaient été faites automatiquement. Sache que "indécidable" veut dire qu'il n'existe pas de procédure automatique permettant de résoudre un problème donné. Il qu'il n'en existera jamais : c'est un fait scientifique.
[^] # Re: Pour vous éviter un clic
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 3.
Car justement le résultat de la compilation n'est pas terrible en prog objet.
Et l'interet du modèle prototype de lisaac est qu'il permet de mettre en place des techniques de compilation plus efficace pasque le langage s'y prete bien.
[^] # Re: Pour vous éviter un clic
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 3.
Je sais bien que c'est ce que fait gtk et personnellement je n'échangerai pas deux barils de gtk contre un baril de qt.
Alors après il y a d'autre avantage a l'utilisation de gtk : binding plus facile avec d'autre langage, compilo plus performant que celui de c++.
Mais justement si on arrive à résoudre ces problèmes je preferai largement programmer en objet.
[^] # Re: Pour vous éviter un clic
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 4.
Ouais mais aucun compilateur ne permet d'utiliser toutes les techniques objet pour du code dont la rapiditée d'exécution est critique. Genre dans ce genre de biblio
Par exemple si tu regarde les autres projets (y'a des liens sur le site de lisaac) de codage d'un os avec un langage objet ils recommandent tous de ne surtout pas utiliser le polymorphisme. du coup on ne voit pas trop l'interet d'utiliser un langage objet. Alors qu'ici le but est bien de ne pas se restreindre et de garder l'efficacitée.
En ce moment c'est a la mode de dire que les concept objet c'est juste une vision de l'esprit et que l'on peut faire de l'objet avec n'importe quel objet.
Alors c'est vrai oui, de la même facon que l'on peut tout réaliser avec n'importe quel langage, ils sont tous turing-complet.
Mais il y aussi indéniable que si on utilise des langages bien adapté a ce que l'on veut faire on arrive plus vite a un meilleur résultat.
Perso je pense que refaire le travail du compilateur tous les jours pasque on essaie de faire de l'objet avec du C, ben c'est une mauvaise idée.
Alors évidement il faut absolument un compilo qui tienne la route, ce qui est le cas ici.
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 3.
D'un autre coté je me souviens pas d'avoir été aussi agressif avec toi !
Cette syntaxe est effectivement tres naturelle.
Mais ceci n'est pas une definition du for mais une utilisation du for comme définie dans la grammaire de caml. Donc ca n'a rien a voir avec mon discours.
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 3.
Et il se repose compltement sur gcc puisque il génére du C avec quelques extension de gcc.
Et quand je disais que c'était comme dans Lisaac, c'est parcque les templates sont réellement des citoyen de premiere classe et que le compilo est déjà efficace.
Et la syntaxe et la sémantique de C++ ne permettront jamais d'avoir un compilo qui génére du code aussi performant que celui de lisaac. t'aura beau mettre 400 personnes dans le projet g++ ca ira pas
Parceque justement un bon paquet d'optimisation automatique dans lisaac sont prévue pour être fait à la main en C++. Et que le langage est trop complexe
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 3.
Mais concernant le troll, je pense qu'au contraire la prochaine fois que j'écrit un journal je vais en inclure 2-3 dedans :) . Regarde, sans le troll sur Ocaml on aurait jamais eu ton commentaire ! Ici ca marche au troll...
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 2.
Comme dans lisaac quoi ? :)
[^] # Re: Pour vous éviter un clic
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 2.
Évidement ca ne change rien au fait que sorti des fonction de base comme drawLine le travail reste compliqué. (je dis ca avant que quelqu'un d'autre le dise :))
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 2.
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 2.
D'un point de vue syntaxe et sémantique on marie des choses par la force. Et au final on se retrouve avec un langage tres tres gros (ML + impératif + classe + module). Perso j'aurai préféré qu'ils gardent la simplicité du langague d'origine, bon ce n'était pas forcement possible
C'est tout a fait l'opposé de la philosophie de lisaac. cf la grammaire http://isaacos.loria.fr/li_docs.html qui est très courte mais le langage reste quand même tres expressif.
Par exemple voici la définition de la boucle for. En fait c'est très proche d'un itérateur sur les entier tel que l'on aurait pus le définir en Caml.
to limit_up:SELF do blc:BLOCK <-
(
(self<=limit_up).if {
blc.value self;
(self+1).to limit_up do blc;
};
);
en caml (pas objet) ca aurait fait un truc du style
let rec for i limit_up blc=
if i<limit_up
then blc i;for (i+1) blc
else blc i
;;
du type int -> int -> (int -> ()) ->() (a vue de nez)
(mon caml est rouillé donc ca doit être faux, mais j'ai pas envie d'installer le compilo)
Je trouve que c'est un exemple très réussit d'intégration de concept plutot fonctionnel à l'intérieur d'un langage objet mais sans rajouter des construction plus ou moins étrangère dans la syntaxe de base. En fait ce qu'il ont eu besoin de rajouter c'est le type BLOCK correspondant a un suite d'instruction séquentielles. Comme ca on peut passer des blocs a itérer au la commande for (enfin to do : on peut définir plusieur mot clef).
[^] # Re: Et c'est où pour tester ?
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 2.
J'aurai du préciser pas trop dur par rapport a l'avancé du projet (il me semble qu'un portage sur ARM a déjà été fait) et a la difficulité des techniques habituelles.
Apres évidement je pense que tout le monde a une idée de la quantité de travail derrière ...
[^] # Re: Pour vous éviter un clic
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 2.
Par contre le compilo lisaac est prévu pour faire du c, donc faudrait en prime refaire tous la partie arrière pour sortir l'asm des shaders.
C'est vrai que cela serait intéressant de voir si le modèle proposé resiste au choc.
[^] # Re: Pour vous éviter un clic
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 2.
Mais les shader ca ce programme pas indépendament du logiciel qui l'utilise avec un espece d'assembleur standard ? j'ai pas l'impression que les shaders ca fait partie du driver mais je suis pas un spécialiste
[^] # Re: Et c'est où pour tester ?
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 2.
Pour le moment on a juste le compilo dans un fichier c généré depuis la version en lisaac. Et isaac (l'os) dans un fichier c aussi généré depuis la version en lisaac. Par contre la lib est dispo en lisaac. (le tout en licence cecill)
Mais ils ont l'air assez ouvert au libre maintenant. Alors je pense qu'il faut mettre la pression jusqu'a ce que ils fournissent le compilo (surtout) et l'os. Histoire qu'ils sentent qu'on est derrière et qu'on est intéressé d'en faire un projet libre.
Pour répondre à ta question techniquement je pense pas que cela soit trop dur, c'est quoi dans un iPaq un ARM ?
[^] # Re: Pour vous éviter un clic
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 2.
Je ne suis pas d'accord c'est plus facile de *bien* faire intéragir le matos avec le driver si on a un langage qui permet d'exprimer plus facilement ce que l'on essaye de faire.
Evidement ca ne change rien de fondamental (rien non plus aux problemes de spec non disponible), mais je pense que la rédaction de driver serai plus rapide de plusieurs ordres de grandeur si on abandonne le C pour un langage plus haut niveau.
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 3.
Lisaac (avec deux a) est beaucoup plus jeune que Ocaml.
Ca ne fait que très recement qu'il y a une version utilisable de Lisaac. En plus le développement a été réalisé par une seule personne (+un ingé pendant 2 ans).
On est au tout début pour Lisaac alors que Ocaml a déjà une longue histoire et est mature.
Perso je trouve que Caml a un bon succes ...pour un langage fonctionel, je ne pense pas qu'on puisse attendre beaucoup plus.
Alors que Lisaac est impératif objet et bien adapté pour faire des choses efficaces.
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 2.
C'est de moins en moins vrai, pour les appli utilisateur desktop oui mais en entreprise ca a beaucoup évolué vers Java. Et cela évoluera encore, c lent mais ca bouge qd même
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 4.
Mais ce n'est pas suffisant ici :
exemple :
let add x y = x + y ;;
Dis moi quelle est le type des paramètres formels x et y suivant ta méthode ? int ou float ?
[^] # Re: Pffff...
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 8.
mdr, c'est sur que faire la différence entre (je veux un entier) 3+4 et (je veux un flottant) 3+4 c'est réalisé par tout les compilo du monde.
C'est exactement pareil pour tout les langage a un moment donné il faut que tu dise au compilo quel type tu veux utiliser. Or il n'y a pas de déclaration de type en Caml donc ils utilisent des opérateur différent "+" et "+.". Dans le contexte c'est la seul manière de faire.
Apparement tu a encore des progres a faire en prog fonctionnelle :)
Sérieusement ce qui est vraiment dommage c'est qu'ils n'ont pas utilisé l'extension objet de OCaml pour définir un type Nombre et uniffier l'interface des opérateurs entre les entiers et les flottants.
Pour en revenir au sujet : ce point la est traité correctement en Lisaac. On manipule les différentes type de nombres (entiers ...) suivant la même interface.
[^] # Re: Autres langages à prototype
Posté par outs . En réponse au journal Un compte rendu de la conf sur isaac/lisaac. Évalué à 3.
Mais lisaac est typé statiquement et compilé, il est donc plutot sur et efficace. Donc il répond à la plupart des critiques.
A part la dernière sur le fait que les developpeur ne sont pas familier avec cette technique. Mais bon ca c'est comme n'importe quel innovation. Genre y'a plein de gens qui sont boulonné au C et qui ne veulent surtout pas changer, quelque soit les arguments qu'on leur donne. A mon avis c'est le peur de quitter un environnement familier où ils exercent un position privilégiée ... surtout quand la nouvelle technique rend caduque un travail autrefois fait à la main !
Mais bon y'a pas de gens comme ça ici ! non ? :)
[^] # Re: Pour vous éviter un clic
Posté par outs . En réponse au journal Lisaac libéré ?!?. Évalué à 1.
[^] # Re: qques questions sur Lissac et... Ruby, Java, Caml...
Posté par outs . En réponse à la dépêche 23 mars: Conférence au LORIA sur Lisaac, un nouveau langage. Évalué à 1.
Et il en existe un sacré paquet pourtant des méthodes ...
alors je considere ca normal d'utiliser tjrs cet exemple et d'en être fier surtout que c'est une étape fondamentale dans l'histoire du B.
Et celui ci a évolué depuis. On est passé au B événementiel et une nouvelle version des outils est en préparation http://rodin-b-sharp.sourceforge.net/ en plus cela sera libre.
[^] # Re: qques questions sur Lissac et... Ruby, Java, Caml...
Posté par outs . En réponse à la dépêche 23 mars: Conférence au LORIA sur Lisaac, un nouveau langage. Évalué à 1.
Plein de cas courant peuvent être résulu, et c'est cela qui nous permet d'écrire des prouveurs, ou de faire marcher des algos de model-checking.
Il n'empeche que même dans les cas courant (de l'industrie) il y a des cas emmerdant qui ne fonctionnent pas avec les techniques actuels. Que cela soit avec le prouveur de B ou n'importe quel autre. La principale limite étant que la complexité de ce genre d'algo est généralement exponentielle. Alors qu'un être humain arrive, plus ou moins, a *voir* la solution directement.
En pratique en B on dirige le prouveur en lui faisant faire des cas intermédiaire et en lui machant le travail. Alors même dans les preuve à la main le prouveur est essentiel.
Perso je trouve que ca marche pas trop mal, bon ok defois on s'arrache les cheveux et sa demande pas mal d'expérience et de temps.
[^] # Re: qques questions sur Lissac et... Ruby, Java, Caml...
Posté par outs . En réponse à la dépêche 23 mars: Conférence au LORIA sur Lisaac, un nouveau langage. Évalué à 1.
je ne vois vraimement pas ce qui te choque ?
[^] # Re: qques questions sur Lissac et... Ruby, Java, Caml...
Posté par outs . En réponse à la dépêche 23 mars: Conférence au LORIA sur Lisaac, un nouveau langage. Évalué à 0.
Et alors ?
Si c'est une réthorique de ta part pour sous-entrendre que le B n'a jamais servis a rien d'autre, je trouve ca mesquin. Je ne vais pas chercher d'autre exemples pour te faire plaisir.
Je n'ai prétendu que toute les preuves avaient été faites automatiquement. Sache que "indécidable" veut dire qu'il n'existe pas de procédure automatique permettant de résoudre un problème donné. Il qu'il n'en existera jamais : c'est un fait scientifique.