Why génère une preuve pour COQ qui se charge dé montrer que l'algo est valide.
Le problème est que COQ n'est pas incrémental.
Il y a plusieurs défis :
1/ Concevoir un générateur de preuve à partir des contrats
2/ Concevoir un système qui vérifie la cohérence des contrats, ie. qu'il n'y ait pas incomplétude.
3/ Prouver le compilateur ou au moins une bonne partie
donc
4/Prouver le langage (sa grammaire)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Comment faire un langage plus rapide que C ?
Posté par Ontologia (site web personnel) . En réponse à la dépêche 23 mars: Conférence au LORIA sur Lisaac, un nouveau langage. Évalué à 4.
C'est dans la lignée des travaux de Jean-Christophe Filliatre
http://why.lri.fr/index.fr.html
Exemple : http://why.lri.fr/examples/sqrt/sqrt.mlw.html
Why génère une preuve pour COQ qui se charge dé montrer que l'algo est valide.
Le problème est que COQ n'est pas incrémental.
Il y a plusieurs défis :
1/ Concevoir un générateur de preuve à partir des contrats
2/ Concevoir un système qui vérifie la cohérence des contrats, ie. qu'il n'y ait pas incomplétude.
3/ Prouver le compilateur ou au moins une bonne partie
donc
4/Prouver le langage (sa grammaire)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker