Voila cela fait plusieur fois que j'utilise se site pour trouver des logiciel libre, et je viens (seulement aujourd'hui) de me rendre comtre du faite que vous ne parliez pas de COQ.
Je vais donc presenter rapidement coq:
-C'est un projet Open source (qui est en cours depuis un certain momment) develope par l'INRIA programme en Ocaml utilisable sous windows, linux (mac je ne me rapelle plus ).
-Coq est un outil d'aide a la demonstration en logique intuitionniste et un langage de programmation pour faire des programmes ceritifies.
Quelques explication au sujet de la logique intuitionniste derriere ce gros mot ce cache une logique proche de la programmation, coq (bon l'utilisateur a l'aide coq) construise ses preuves comme des programmes informatiques (pour les plus interresses: il se cache derriere coq l'isomorphisme de Curry-Howard).
Notes personnelles: apres un apprentissage qui necessite quelques efforts il est amusant de prouver des theoremes en coq et de generer des preuves formelles.
Je pense que pour les passionne de math et d'informatique ce logiciel me semble amusant voir passionnant d'autant plus que la communaute des utilisateurs de coq s'attaque a de gros probleme: theoreme des quatres couleur (resolu) conjecture de kepler (en cours).
Autre remarque: personellement j'utilise coqide comme ide (il est lui aussi open source et developer par l'INRIA) mais il existe aussi l'environement emacs: proofgeneral qui a plus de fonctionalite a ce que je me rappel.
Voila je pense qu'il serai bien que votre site repertorie ce logiciel attention tout de meme utilise coq sans ide releve vite de la haute voltige. A noter: il existe des paquages debian pour coq coqide et prouvegeneral. Pourriez-vous si vous ne desire pas reference ce logiciel m'en donnez les raisons merci.
voici l'adresse du site [url]coq.inria.fr[/url]
PS:je suis desole pour les accents mais etant actuellement en Angletere, j'utilise un clavier anglais et donc sans accents merci de votre Comprehension.
Je vais donc presenter rapidement coq:
-C'est un projet Open source (qui est en cours depuis un certain momment) develope par l'INRIA programme en Ocaml utilisable sous windows, linux (mac je ne me rapelle plus ).
-Coq est un outil d'aide a la demonstration en logique intuitionniste et un langage de programmation pour faire des programmes ceritifies.
Quelques explication au sujet de la logique intuitionniste derriere ce gros mot ce cache une logique proche de la programmation, coq (bon l'utilisateur a l'aide coq) construise ses preuves comme des programmes informatiques (pour les plus interresses: il se cache derriere coq l'isomorphisme de Curry-Howard).
Notes personnelles: apres un apprentissage qui necessite quelques efforts il est amusant de prouver des theoremes en coq et de generer des preuves formelles.
Je pense que pour les passionne de math et d'informatique ce logiciel me semble amusant voir passionnant d'autant plus que la communaute des utilisateurs de coq s'attaque a de gros probleme: theoreme des quatres couleur (resolu) conjecture de kepler (en cours).
Autre remarque: personellement j'utilise coqide comme ide (il est lui aussi open source et developer par l'INRIA) mais il existe aussi l'environement emacs: proofgeneral qui a plus de fonctionalite a ce que je me rappel.
Voila je pense qu'il serai bien que votre site repertorie ce logiciel attention tout de meme utilise coq sans ide releve vite de la haute voltige. A noter: il existe des paquages debian pour coq coqide et prouvegeneral. Pourriez-vous si vous ne desire pas reference ce logiciel m'en donnez les raisons merci.
voici l'adresse du site [url]coq.inria.fr[/url]
PS:je suis desole pour les accents mais etant actuellement en Angletere, j'utilise un clavier anglais et donc sans accents merci de votre Comprehension.
-
lambda
- Messages : 1