Fondements logiques pour la méta-programmation avec typage sûr

1. Résumé du projet

La méta-programmation permet au programmeur d’écrire des programmes qui génèrent du code optimisés et spécialisé.  Cela offre l’opportunité d’exploiter les connaissances spécifiques au domaine, pour complémenter les optimisations génériques que le compilateur emploie et produire ainsi des programmes à hautes performances.  Malheureusement, écrire des méta-programmes sûrs et fiables est encore un défi souvent frustrant, vu que les techniques de test habituelles ne peuvent s’appliquer qu’aux programmes générés et non au méta-programme.  Pour faciliter l’écriture de méta-programmes, des outils qui permettent de détecter les erreurs directement dans le méta-programme – plutôt que dans le code généré – sont essentiels.

Notre recherche vise à développer les fondements logiques pour la méta-programmation typée sure. Concrètement, notre but est triple :

1. S’assurer que l’on peut facilement et correctement manipuler et combiner des fragments de code générés ;
2. Fournir au programmeur les abstractions nécessaires pour pouvoir simplement et efficacement analyser et optimiser les fragments de code ;
3. Rendre la certification que le code généré sera correct une tâche banale.

Ceci mènera à des méta-programmes plus fiables et accélérera le développement en réduisant le temps passé à les débogguer. Idéalement, presque tout le déboggage peut être fait statiquement, avant même d’exécuter le code, plutôt que bien plus tard dans des batteries de tests.  À long terme, cela facilitera l’écriture de méta-programmes.  Cela permettra ainsi de mieux tirer profit de la méta-programmation sans sacrifier la fiabilité de et la confiance en les logiciels.