Un des points essentiel du projet œuf est que les programmes peuvent manipuler d'autres programmes. Il y a fonction d'évaluation qui permet de prendre un bout de programme et de l'exécuter. Je te rappelle qu'une des notions fondamentales est celle de type. Un type permet de décrire ce à quoi correspond un emplacement mémoire. Par exemple, il y a les types nombre, cercle, ou encore fonction qui prend un nombre et renvoie une liste de nombres. Le projet œuf ajoute une nouvelle famille de types que j'appelle les types boîtes pour l'instant. Une boîte de type T est une valeur qui une fois exécuté donne une valeur de type T. J'essaierai de mieux expliquer à l'avenir.
Je suis en train d'implémenter l'algorithme de typage. Je code deux fois les mêmes choses, une fois pour les boîtes et une autre pour les expressions normales. Je sais qu'il y a des techniques pour faire mieux, dans d'autres cadres plus structurés. Je ne sais pas s'ils s'appliqueront ici. Dans tous les cas, j'espère faire mieux.
Des nouvelles du front ! J'ai écrit dans Coq les règles que j'avais en tête pour une version simplifiée d'œuf : le fragment simplement typé. Je vais maintenant essayer de prouver deux propriétés essentielles :le progrès et la préservation. La combinaison de ces deux propriétés assure que le typage fait ce qu'on lui demande. C'est-à-dire qu'un programme bien typé n'a pas de bogues à l'exécution.
En fait j'ai oublié de définir la sémantique ! Je ne peux pas encore commencer les preuves. Oublier la sémantique c'est déjà ce que l'anonyme avait reproché à mon rapport de stage.