Pour ceux qui ne connaissent pas ces notions, disons qu'on peut par exemple exprimer dans le système de types de Coq que l'on définit une fonction qui prend un entier et renvoie son double. Autrement dit on peut exprimer complètement la sémantique du code, et le système vérifie que le code correspond bien à sa sémantique. D'une certaine façon, un code Coq qui compile est garantie sans bugs.
Dans quel types de contexte est-ce que coq est utilisé. J'avais lu des articles concernant des utilisations dans les transactions bancaires, il s'agissait d'un exemple essentiellement académique sur un très petit sous-système. Du coup je n'ai pas trop d'intuition sur la taille des programmes qu'on peut pratiquement prouver avec coq. Est-il facile de travailler sur les appels-système, comme par exemple pour démontrer dans un programme que toutes les conditions d'erreur sont correctement traitées?
Est-ce que tu sais ce que devient focal?
Enfin, je ne suis pas logicien, mais mathématicien, du coup j'ai essayé de me mettre dans la peau do coq. La première seconde, je me suis dit, "hey chouette:"
Il existe x tel que P <-> Il existe un programme calculant x tel que P
par contre pour transformer le pour tout en logique intuitionniste, j'ai moins fait le malin puisque la formulation
pour tout x on a P <-> Non(Il existe x tel que Non P) <-> Il n'existe aucun programme calculant x tel que non P
me paraît préparer beaucoup de problème à celui qui voudrait s'en servir. :) Du coup que font les intuitionnistes pour traduire les énoncés en "pour tout"? Est-ce que c'est ce "second ordre" que j'ai jusqu'ici négligé qui sauve les meubles? Ou bien est-ce qu'ils se lancent dans des considérations énumératives?
[^] # Re: Le web
Posté par Michaël (site web personnel) . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 4.
Dans quel types de contexte est-ce que coq est utilisé. J'avais lu des articles concernant des utilisations dans les transactions bancaires, il s'agissait d'un exemple essentiellement académique sur un très petit sous-système. Du coup je n'ai pas trop d'intuition sur la taille des programmes qu'on peut pratiquement prouver avec coq. Est-il facile de travailler sur les appels-système, comme par exemple pour démontrer dans un programme que toutes les conditions d'erreur sont correctement traitées?
Est-ce que tu sais ce que devient focal?
Enfin, je ne suis pas logicien, mais mathématicien, du coup j'ai essayé de me mettre dans la peau do coq. La première seconde, je me suis dit, "hey chouette:"
Il existe x tel que P <-> Il existe un programme calculant x tel que P
par contre pour transformer le
pour touten logique intuitionniste, j'ai moins fait le malin puisque la formulationpour tout x on a P <-> Non(Il existe x tel que Non P) <-> Il n'existe aucun programme calculant x tel que non P
me paraît préparer beaucoup de problème à celui qui voudrait s'en servir. :) Du coup que font les intuitionnistes pour traduire les énoncés en "pour tout"? Est-ce que c'est ce "second ordre" que j'ai jusqu'ici négligé qui sauve les meubles? Ou bien est-ce qu'ils se lancent dans des considérations énumératives?