Ce n'est qu'une solution qui doit être mise en synergie avec d'autres, puisque la méthode ultime n'existe pas (foutu théorème de Rice).
On peut s'en approcher, par exemple, si on réussit à programmer et prouver en Coq 99% (pourcentage à la louche) du programme dans les restrictions imposées par un langage non Turing-complet. Il restera, bien sûr, toujours un 1% où d'autres méthodes seront nécessaires. Après, je ne pense pas qu'il y ait beaucoup de programmes en dehors des systèmes vraiment critiques pour lesquels une telle approche soit raisonnable.
[^] # Re: Méthodes formelles
Posté par anaseto . En réponse à la dépêche [code] Trouver les erreurs. Évalué à 3.
On peut s'en approcher, par exemple, si on réussit à programmer et prouver en Coq 99% (pourcentage à la louche) du programme dans les restrictions imposées par un langage non Turing-complet. Il restera, bien sûr, toujours un 1% où d'autres méthodes seront nécessaires. Après, je ne pense pas qu'il y ait beaucoup de programmes en dehors des systèmes vraiment critiques pour lesquels une telle approche soit raisonnable.