Et on fait quoi de l'Atelier B ? Parce qu'un prof me soutenait que ça permettait de faire des choses sans faille, une fois qu'on avait tout prouvé par ce truc.
Oui, tu peux prouver formellement qu'un programme est conforme à une modélisation. Ensuite, il peut toujours y avoir des erreurs dans la modélisation (mais c'est vrai qu'il est plus facile de se "convaincre" de l'exactitude d'une modélisation que de celle d'un programme). Et le prouveur peut aussi être buggé, mais là ça serait vraiment pas de chance ;).
[^] # Re: Faille sendmail et vulnérabilité OpenSSH
Posté par Pierre Tramo . En réponse à la dépêche Faille Sendmail et vulnérabilité OpenSSH. Évalué à 3.
Oui, tu peux prouver formellement qu'un programme est conforme à une modélisation. Ensuite, il peut toujours y avoir des erreurs dans la modélisation (mais c'est vrai qu'il est plus facile de se "convaincre" de l'exactitude d'une modélisation que de celle d'un programme). Et le prouveur peut aussi être buggé, mais là ça serait vraiment pas de chance ;).