Il y a un débat assez proche sur la modularité au niveau purement théorique de la construction des preuves de sûreté des langages. Les techniques de preuve par induction sur les dérivations de typage sont assez simples (... quand on a tous les invariants qui vont bien qui sont exprimés par la syntaxe, ce qui est parfois loin d'être simple ou même pas bien compris du tout), mais pas contre il faut en théorie les refaire à chaque fois qu'on modifie un peu le langage, on ne peut pas prouver les constructions une par une de façon modulaire—d'ailleurs les assistants de preuve aident dans ce cas à vérifier rapidement que le reste de la preuve marche toujours. En contraste les techniques de preuves plus sémantiques comme la réalisabilité ou les relations logiques, ou en général par modèles, ont un aspect plus modulaire, puisque les constructions sont montrées admissibles une par une, et en ajouter une nouvelle ne demande pas de reprendre l'existant. Par contre elles sont nettement plus lourdes à mettre en place, et elles fixent quand même un univers de discours qu'il faut modifier et reconstruire quand on introduit des constructions vraiment différentes (enfin dans la syntaxe aussi).
[^] # Re: Tagless final un chemin vers MetaOCaml en bibliothèque ?
Posté par gasche . En réponse au journal Découvrir MetaOCaml dans son navigateur. Évalué à 3.
Il y a un débat assez proche sur la modularité au niveau purement théorique de la construction des preuves de sûreté des langages. Les techniques de preuve par induction sur les dérivations de typage sont assez simples (... quand on a tous les invariants qui vont bien qui sont exprimés par la syntaxe, ce qui est parfois loin d'être simple ou même pas bien compris du tout), mais pas contre il faut en théorie les refaire à chaque fois qu'on modifie un peu le langage, on ne peut pas prouver les constructions une par une de façon modulaire—d'ailleurs les assistants de preuve aident dans ce cas à vérifier rapidement que le reste de la preuve marche toujours. En contraste les techniques de preuves plus sémantiques comme la réalisabilité ou les relations logiques, ou en général par modèles, ont un aspect plus modulaire, puisque les constructions sont montrées admissibles une par une, et en ajouter une nouvelle ne demande pas de reprendre l'existant. Par contre elles sont nettement plus lourdes à mettre en place, et elles fixent quand même un univers de discours qu'il faut modifier et reconstruire quand on introduit des constructions vraiment différentes (enfin dans la syntaxe aussi).