Re: À boire et à manger

Ben c’est indécidable, il me semble, parce qu’il faudrait détecter les points de code inaccessibles.

Je me rend compte que j'étais resté trop évasif sur ma notion de nécessaire, j'entendais par là la nécessité au sens de l'approximation conservative telle que définie dans ton lien. Est nécessaire tout ce qui est potentiellement appelé, même sous une condition dynamique qui ne peut jamais terminée.

Mais je dois être biaisé dans mon appréhension de la difficulté, d'après Nicolas Boulay le linker de Gcc effectue ces suppressions (quoi que ça ne signifie pas que le problème soit simple à résoudre).

Pour illustrer ce que j'ai en tête, je l'illustre avec un exemple en programmation modulaire. Imaginons qu'on a un module de List avec cette signature :

module type LIST = sig
 type 'a t
 val nil : 'a t
 val singleton : 'a -> 'a t
 val cons : 'a -> 'a t -> 'a t
 val hd : 'a t -> 'a
 val tl : 'a t -> 'a t
 val append : 'a t -> 'a t -> 'a t
 val map : ('a -> 'b) -> 'a t -> 'b t
 val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
 val flatten : ('a t) t -> 'a t
end

Un tel module définit le concept de liste chaînée, ainsi que quelques propositions de base sur lui (une théorie élémentaire sur les listes, en somme). Maintenant, je veux écrire un programme qui utilise ce concept mais le seul théorème qui m'intéresse est que l'on peut mapper une liste. Problème pour le compilateur : faire en sorte que seul le code de List.map soit lié statiquement à mon binaire, mon programme n'ayant rien à faire du fait que l'on puisse aplatir une liste de listes par exemple.

On retrouve le même genre de questions dans les langages orientés objets (un objet c'est le module du pauvre) : ne pas lier statiquement le code des méthodes dont on est certain qu'elles ne seront jamais appelées.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.