Ce qui est indécidable c'est de savoir si le cas où le dénominateur est égal à zéro peut se produire ou pas. C'est à cet énoncé que le théorème de Rice s'applique.
Là tu cherche à prouver automatiquement qu'un code ne fera jamais de division par 0 ce qui n'est pas le sujet. Le sujet c'est de gérer le cas d'une division par 0. C'est aussi un sophisme le jusqueboutisme pour invalider ;)
Et oui j'ai bien dis dès mon premier commentaire que ça a un coût.
Ce qu'on trouve au mieux en pratique, c'est des outils qui font des analyses statiques pour vérifier qu'un code respecte des pratiques particulières (c'est-à-dire utilise un sous-ensemble du langage et pas le langage en général), et lorsque c'est le cas, elles peuvent nous assurent l'absence de division par zéro. C'est le genre d'approche qu'on retrouve dans certains codes critiques.
Ou par preuve automatique ou pas écriture par automate (tu écris dans un méta langage qui va produire un code ayant forcément certaines propriétées).
[^] # Re: Ouaiche
Posté par barmic 🦦 . En réponse au lien "Rust vs. Go: Why They’re Better Together". Évalué à 3.
Là tu cherche à prouver automatiquement qu'un code ne fera jamais de division par 0 ce qui n'est pas le sujet. Le sujet c'est de gérer le cas d'une division par 0. C'est aussi un sophisme le jusqueboutisme pour invalider ;)
Et oui j'ai bien dis dès mon premier commentaire que ça a un coût.
Ou par preuve automatique ou pas écriture par automate (tu écris dans un méta langage qui va produire un code ayant forcément certaines propriétées).
https://linuxfr.org/users/barmic/journaux/y-en-a-marre-de-ce-gros-troll