On pourrait considérer la paire (programme, spécification) comme le programme (un programme annoté), mais la propriété que l'on veut vérifiée n'est pas exprimable en terme du langage reconnu par le programme annoté, ou plus généralement du comportement observable du programme annoté.
et donc les argumentations diagonales à la Cantor ne s'appliquent pas.
À la lecture de la réponse que tu as eu, j'abandonne la controverse. La prochaine fois j'éviterai les boutades sur Popper, tout est parti de là, d'autant que le recours à Popper semble se restreindre à la réfutation par le contre-exemple : si un test ne passe pas alors on a un contre-exemple donc le code n'est pas conforme à sa spécification1 (quand bien même elle n'est exprimée qu'informellemement); l'humanité n'a tout de même pas attendu Popper pour tenir ce genre de raisonnement.
Initialement je pointais du doigt l'inférence de type et son lien avec la déduction naturelle, ce que l'on peut faire automatiquement (sans annotation particulière du développeur, ni intervention de sa part dans le processus de dérviation) pour en pointer les limites (le théorème de Rice, si ça lui plaît) et là on a le droit à :
Je n'ai jamais dit que tous les problèmes non triviaux étaient indémontrables, j'ai seulement dit certain et cela depuis le début (bon effectivement ma phrase peut être perçu de manière ambigüe « des » signifie ici certain et non pas tous) et automatiquement (ie. par un compilateur générique)
Ce que personne n'a jamais nié, c'est même cette limite que je pointais du doigt. Il ne veut pas entendre que les conditions d'application du théorème sont dépassables (annotation, dérivation humaine avec assistance de la machine, système de types plus riche que le système F...), et donc que là où n'est pas la condition, là n'est pas le conditionné, i.e la conclusion du théorème.
Comme, de plus, j'interprète tous les problèmes autour du typage du lambda-calcul à travers le prisme de la correspondance de Curry-Howard, j'ai du mal à considérer la démonstration de théorèmes comme une science expérimentale et je suis du genre compilateur très pointilleux quand il s'agit d'en faire usage.
à ne pas confondre avec si tout les tests passent alors le code est conforme, sauf si les tests sont exhaustifs ce qui est impossible quand ils sont infinis; à moins de tester exhaustivement, non sur les instances des entrées, mais sur leur forme ce qui peut se faire en temps fini et ce que font les assistants de preuves. ↩
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é à 0.
Pas mieux !
et donc les argumentations diagonales à la Cantor ne s'appliquent pas.
À la lecture de la réponse que tu as eu, j'abandonne la controverse. La prochaine fois j'éviterai les boutades sur Popper, tout est parti de là, d'autant que le recours à Popper semble se restreindre à la réfutation par le contre-exemple : si un test ne passe pas alors on a un contre-exemple donc le code n'est pas conforme à sa spécification1 (quand bien même elle n'est exprimée qu'informellemement); l'humanité n'a tout de même pas attendu Popper pour tenir ce genre de raisonnement.
Maintenant, on constate une technique du genre extension-restriction : le premier stratagème dans l'Art d'avoir toujours raison, avec un soupçon de « je mets de l'eau dans mon vin » sans en avoir l'air.
Initialement je pointais du doigt l'inférence de type et son lien avec la déduction naturelle, ce que l'on peut faire automatiquement (sans annotation particulière du développeur, ni intervention de sa part dans le processus de dérviation) pour en pointer les limites (le théorème de Rice, si ça lui plaît) et là on a le droit à :
Ce que personne n'a jamais nié, c'est même cette limite que je pointais du doigt. Il ne veut pas entendre que les conditions d'application du théorème sont dépassables (annotation, dérivation humaine avec assistance de la machine, système de types plus riche que le système F...), et donc que là où n'est pas la condition, là n'est pas le conditionné, i.e la conclusion du théorème.
Comme, de plus, j'interprète tous les problèmes autour du typage du lambda-calcul à travers le prisme de la correspondance de Curry-Howard, j'ai du mal à considérer la démonstration de théorèmes comme une science expérimentale et je suis du genre compilateur très pointilleux quand il s'agit d'en faire usage.
à ne pas confondre avec si tout les tests passent alors le code est conforme, sauf si les tests sont exhaustifs ce qui est impossible quand ils sont infinis; à moins de tester exhaustivement, non sur les instances des entrées, mais sur leur forme ce qui peut se faire en temps fini et ce que font les assistants de preuves. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.