Contenu de robocop
Il y a 2 élément(s) pour robocop (recherche limitée depuis 04-mai 13)
Par type de contenu
Plus de filtres
-
La vraie IA... A ne pas confondre avec la fauss...
Je lirais attentivement ton second article car pour l'instant je ne vois pas trop comment ce logiciel fonctionne.
Concernant Coq, lorsque le logiciel te dis "ça y est c'est prouvé" et si tu ne t'es pas trompé dans la spécification du programme à prouver, alors il n'y aura pas de bogue. Ce logiciel commence à être utilisé dans des domaines critiques (ex nucléaire), par exemple avec le compilateur C Compcert dont on a apporté la preuve qu'il ne peut pas produire de bogue en compilant.
Si tout le monde n'utilise pas Coq (ou autre) c'est parce que prouver un programme c'est très long.- juil. 03 2011 10:52
- par robocop
-
La vraie IA... A ne pas confondre avec la fauss...
Si l'on est pas un expert comme moi, c'est difficile de voir ou "Maïeutique" se situe. Est-ce que c'est un langage similaire à prolog par exemple ?
"8ème défaut du procédural : impossible de certifier la fiabilité du programme écrit (théorème de Gödel)"
C'est faux et on dispose maintenant d'assistants de preuves (comme Coq) pour prouver qu'un programme fait ce qu'on lui demande (bien sur il ne faut pas se tromper sur sa spécification ie il faut bien formaliser le comportement attendu).
D'autre part l'article présente l'informatique comme deux mondes distincts, le procédural et l'ia.
Amha vous oubliez quand même certaines catégories de langages comme le fonctionnel (cf ocaml ou haskell) ou encore les langages distribués comme erlang (qui grâce a des concepts comme le "hot code swapping" contestent l'argument "impossible de modifier un programme en cours d’utilisation").- juin 30 2011 08:50
- par robocop
