Oula, il ne faut pas prendre la mouche. Mes reproches concernant l'epistémologie popperienne ne consistent pas simplement à dire qu'elle ne s'applique pas aux maths (je sais bien distinguer une science pure, d'une science expérimentale ;-). Mais là, le fil n'est pas un débat sur l'épistémologie : je pourrais, par exemple, lui reprocher plus précisément de ne pas porter assez attention aux principes non mathématiques, mais tout aussi purs, qui sont à la base des sciences expérimentales (principes métaphysiques) et qui échappent à sa démarche de falsification; ou bien de reconnaître, de son propre aveu, d'avoir emprunter sa conception de l'objet à Kant et celle de la vérité à Tarski alors qu'au fond Tarski ne dit rien de plus que Kant sur la notion de vérité, et que j'ai du mal à voir comment on peut comprendre sa conception de l'objet sans celle qu'il avait de la vérité (et donc, quel est l'intérêt de Tarski ?).
Je sais ce que sont les logiques classiques et intuitionnistes et leur rapport aux systèmes de typage : je l'ai déjà exposé ici; et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.
Pour le troisième point, cela dépend : voir également mon commentaire cité au paragraphe précédent, ainsi que certains messages autour de la discussion qui l'a engendré (entre autre, pourquoi on ne peut pas se passer de tests unitaires en OCaml, mais qu'ils ne servent a priori à rien en Coq).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par kantien . En réponse à la dépêche OCaml 4.03. Évalué à 1.
Oula, il ne faut pas prendre la mouche. Mes reproches concernant l'epistémologie popperienne ne consistent pas simplement à dire qu'elle ne s'applique pas aux maths (je sais bien distinguer une science pure, d'une science expérimentale ;-). Mais là, le fil n'est pas un débat sur l'épistémologie : je pourrais, par exemple, lui reprocher plus précisément de ne pas porter assez attention aux principes non mathématiques, mais tout aussi purs, qui sont à la base des sciences expérimentales (principes métaphysiques) et qui échappent à sa démarche de falsification; ou bien de reconnaître, de son propre aveu, d'avoir emprunter sa conception de l'objet à Kant et celle de la vérité à Tarski alors qu'au fond Tarski ne dit rien de plus que Kant sur la notion de vérité, et que j'ai du mal à voir comment on peut comprendre sa conception de l'objet sans celle qu'il avait de la vérité (et donc, quel est l'intérêt de Tarski ?).
Je sais ce que sont les logiques classiques et intuitionnistes et leur rapport aux systèmes de typage : je l'ai déjà exposé ici; et oui, on peut transposer une preuve intuitionniste de l'irrationnalité de racine de 2 dans un système de typage : en la formalisant en Coq, par exemple.
Pour le troisième point, cela dépend : voir également mon commentaire cité au paragraphe précédent, ainsi que certains messages autour de la discussion qui l'a engendré (entre autre, pourquoi on ne peut pas se passer de tests unitaires en OCaml, mais qu'ils ne servent a priori à rien en Coq).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.