Pour moi, il y a un intérêt clair à savoir utiliser ce genre d'outils.
On ne programme pas de la même façon selon qu'on doit ou non prouver son code. Exemple tout con: quand tu écris une boucle while, as-tu toujours en tête un variant qui va décroître et t'assurer que tu vas sortir de cette boucle ? Chaque fonction a une spécification bien définie ?
Si tu programmes comme si tu devais prouver, tu structureras sans doute ton code différemment et le résultat sera vraisemblablement moins bugué.
[^] # Re: Idris
Posté par fmaz fmaz . En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 5.
Pour moi, il y a un intérêt clair à savoir utiliser ce genre d'outils.
On ne programme pas de la même façon selon qu'on doit ou non prouver son code. Exemple tout con: quand tu écris une boucle while, as-tu toujours en tête un variant qui va décroître et t'assurer que tu vas sortir de cette boucle ? Chaque fonction a une spécification bien définie ?
Si tu programmes comme si tu devais prouver, tu structureras sans doute ton code différemment et le résultat sera vraisemblablement moins bugué.