On illustre l'utilisation des règles de Hoare en prouvant l'algorithme calculant la factorielle. Ce développement peut être aussi l'occasion également de parler des difficultés principales pour l'automatisation des preuves utilisant ce système.