On ne peut pas prouver que tous les algorithmes sont corrects. Il faut les contraindre à accepter tout un tas de paramètres pour rendre l'espace de recherche pour la preuve acceptable. Et puis aussi, si ce que tu avances est vrai, on pourrait prédire quand un algo se termine dans le cas général, ce qui n'est pas possible (le problème de l'arrêt est indécidable).
[^] # Re: Implémentation prouvée
Posté par lasher . En réponse au journal OpenSSL est mort, vive (le futur) LibreSSL. Évalué à 5.
On ne peut pas prouver que tous les algorithmes sont corrects. Il faut les contraindre à accepter tout un tas de paramètres pour rendre l'espace de recherche pour la preuve acceptable. Et puis aussi, si ce que tu avances est vrai, on pourrait prédire quand un algo se termine dans le cas général, ce qui n'est pas possible (le problème de l'arrêt est indécidable).