Enfin le problème c'est que le théorème de Rice nous dit qu'on ne peut pas montrer (automatiquement) des théorèmes non triviaux sur les programmes ; donc les preuves mathématiques ne sont pas suffisante en informatique et donc on à besoin de se convaincre que les programmes que l'on fait tourner sont correctes
J'ai oublié, d'en parler, le « donc » peut effectivement gêner car il représente un joli raccourci. Est-ce qu'il sera possible un jour d'écrire des programmes complets, concurrent, temps réel en même temps que leur preuve sans que le coût à payer soit trop lourd ? Le théorème de Rice ne le dit effectivement pas, il dit simplement que même pour des propriétés simples (l'absence d'exception à l'exécution) on a même pas de solution simple (répondre à cette question pendant la compilation).
Alors oui, on pourrait avoir des solutions pas trop moche pour autant, mais pour l'instant on a toujours pas de solution pragmatique simple à l'impossibilité soulevé par le théorème de Rice (comment prouver simplement certaines propriétés importante). Résumer ça en un simple « donc » est effectivement un peu cavalier car ça parle plus d'état de l'art que de résultats théoriques.
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par Diagonale de Cantor (site web personnel) . En réponse à la dépêche OCaml 4.03. Évalué à 2.
J'ai oublié, d'en parler, le « donc » peut effectivement gêner car il représente un joli raccourci. Est-ce qu'il sera possible un jour d'écrire des programmes complets, concurrent, temps réel en même temps que leur preuve sans que le coût à payer soit trop lourd ? Le théorème de Rice ne le dit effectivement pas, il dit simplement que même pour des propriétés simples (l'absence d'exception à l'exécution) on a même pas de solution simple (répondre à cette question pendant la compilation).
Alors oui, on pourrait avoir des solutions pas trop moche pour autant, mais pour l'instant on a toujours pas de solution pragmatique simple à l'impossibilité soulevé par le théorème de Rice (comment prouver simplement certaines propriétés importante). Résumer ça en un simple « donc » est effectivement un peu cavalier car ça parle plus d'état de l'art que de résultats théoriques.