Lazi

Quelles sont les fonctionnalités de la vérification des types ?

Contexte

Sans vérification des types il est pénible de créer un programme, il est donc nécessaire de créer rapidement la vérification des types.

Question

Quels sont les fonctionnalités que le système Lazi de vérification des types doit apporter ?

Étude

Un système de vérification des types sert à vérifier des propriétés sur le code source. D'une part on déclare les propriétés que le source doit vérifier et d'autre part un système de vérification cherche à les vérifier.

Il est nécessaire qu'en cas de non vérification il soit reporté les informations nécessaire à la compréhension du problème.

La vérification des types est une activité qui peut être vue facilement sous un angle mathématique.

Les systèmes courants se contentent de vérifications qui peuvent être faites automatiquement, au prix de limiter l'expressivité des contraintes à vérifier. Il serait bien ici de ne pas limiter l'expressivité des contraintes et, au cas où un système automatique de démonstration ne puisse arriver à la conclusion, donner suffisament d'informations sur les vérités qui n'ont pu être démontrées.

Réponse

  • La déclaration des types se fait sous forme de phrases mathématique exprimant des contraintes sur des formules.
  • L'expressivité de ces phrases mathématiques n'est pas limitée.
  • Un système de preuve automatique doit chercher à vérifier les contraintes.
  • Ce système doit reporter des messages d'erreurs suffisamment aidant.
  • Ce système peut se faire aider grâce à la déclaration de partie de preuve.
  • Il me semble bon d'accepter que le type soit déclaré avant la définition de la chose, comme c'est le cas dans les langages informatiques traditionnels.