Bonjour à tous.
InOCamlWeTrust --> Merci pour les informations à propos d'Airbus. C'est tout à fait intéressant.
Par contre, j'ai une petite remarque à faire sur ton discours. Il faudrait savoir ce que signifie ``prouver un compilateur''. Je sais ce que veut dire ``prouver un énoncé'', mais ``prouver un compilateur'' n'est pas tout à fait clair. Cela veut certainement dire prouver un certain énoncé en rapport avec le compilateur, mais lequel ?
Par ailleurs, en ce qui concerne le fait de se prouver soi-même, le second théorème d'incomplétude de Gödel dit qu'un système qui prouve sa propre consistance ne peut être qu'inconsistant. Evidemment, prouver un compilateur n'est peut-être pas la même chose que prouver une consistance logique. Mais quand même, il me semble que prouver Coq en Coq ne prouve rien, où alors, il y a un élément externe participant à cette preuve.
Par ailleurs, le fait qu'un problème soit NP complet n'empêche nullement de le résoudre, même en supposant P != NP, pourvu que les données ne soient pas trop volumineuses et qu'on dispose d'assez de temps. C'est certainement ce qu'il se passe en patique avec LUSTRE. Il serait intéressant d'obtenir des détails (puisque tu sembles avoir tes entrées chez Airbus) sur les temps mis par les compilateurs LUSTRE pour optimiser les automates d'une taille donnée.
Partager