La preuve de programme sert à montrer qu’un programme est correct vis-à-vis de ce qu’on veut lui faire faire. Pour ça on fait des maths sur un langage avec ses types et ses termes et structures de contrôle.
La preuve tout court sert à montrer qu’un raisonnement est correct pour démontrer une propriété. Pour ça dans les assistant de preuve on utilise des ... types pour coder les propriétés en question. Cf. La leçon inaugurale de Xavier Leroy par exemple, mais il y a d’autres ressources. Et on écrit la preuve comme on écrirait un programme mais avec une logique un peu différente. Et une fois qu’on a fait ça dans certain cas on peut ... compiler la preuve pour avoir un programme exécutable et correct : https://coq.inria.fr/refman/addendum/extraction.html
[^] # Re: Et l'informatique aussi
Posté par thoasm . En réponse au lien Déboguer ... les maths. . Évalué à 3.
Tout à fait d’ailleurs les domaines sont liés :
La preuve de programme sert à montrer qu’un programme est correct vis-à-vis de ce qu’on veut lui faire faire. Pour ça on fait des maths sur un langage avec ses types et ses termes et structures de contrôle.
La preuve tout court sert à montrer qu’un raisonnement est correct pour démontrer une propriété. Pour ça dans les assistant de preuve on utilise des ... types pour coder les propriétés en question. Cf. La leçon inaugurale de Xavier Leroy par exemple, mais il y a d’autres ressources. Et on écrit la preuve comme on écrirait un programme mais avec une logique un peu différente. Et une fois qu’on a fait ça dans certain cas on peut ... compiler la preuve pour avoir un programme exécutable et correct : https://coq.inria.fr/refman/addendum/extraction.html