Du coup je n'ai pas trop d'intuition sur la taille des programmes qu'on peut pratiquement prouver avec coq.
Les trucs publics les plus gros sur le versant informatique que je connaisse en Coq sont Compcert et Bedrock, respectivement un compilateur C prouvé et un cadriciel de preuve de programmes. Bon, en pratique les limites de la scalabilité en Coq ne sont pas trop là où on s'attend, et des problèmes pratiques débiles te sautent à la figure avant d'atteindre des frontières techniques.
par contre pour transformer le pour tout en logique intuitionniste, j'ai moins fait le malin
Je vois pas très bien ce que tu veux dire. Un terme de type ∀x : A. P est une fonction prenant en argument un terme t de type A et renvoyant du P[t]...
[^] # Re: Le web
Posté par Perthmâd . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 2.
Les trucs publics les plus gros sur le versant informatique que je connaisse en Coq sont Compcert et Bedrock, respectivement un compilateur C prouvé et un cadriciel de preuve de programmes. Bon, en pratique les limites de la scalabilité en Coq ne sont pas trop là où on s'attend, et des problèmes pratiques débiles te sautent à la figure avant d'atteindre des frontières techniques.
Je vois pas très bien ce que tu veux dire. Un terme de type ∀x : A. P est une fonction prenant en argument un terme t de type A et renvoyant du P[t]...