Re: Et pendant ce temps, CamlLight poursuite sa route...

Peut on prouver faux dans un système de typage ?

S'il n'est pas dédié à la preuve oui:

 let rec f () = f () in f () : 'a . 'a

qui prouve (forall P, P) (pour une certaine notion de quantification sur les prédicats). S'il est dédié à la preuve, il faut espérer que non. Sinon, tu obtiens une logique dont le seul modèle est à un point... pas très intéressant du point de vue logique.

Il me semblait que le "faux" se traduisait par une exception à l'exécution, ou un programme que ne termine pas. Dans le cas de racine de deux, c'est une fraction qu'on simplifie infiniment par exemple.

Il y a en effet des liens assez forts entre terminaison et consistance logique --- même s'il n'est pas forcément nécessaire d'avoir l'un pour avoir l'autre. À noter que dans mon exemple OCaml, j'ai utilisé la non-terminaison pour prouver (forall P, P).

Mais peut on créer un fonction de type dont le type de retour est "faux" ?

Une fonction qui retourne faux n'est pas problématique. C'est de pouvoir l'appliquer qui pose problème... car tu obtiens alors une preuve de faux. E.g., en Coq:

Definition f (p : False) := p.

est de type (False -> False), qui est une tautologie.