Garantir que les programmes avec des boucles font ce que nous voulons
Les boucles, en programmation, sont ce qui permet à un ordinateur de répéter inlassablement la même tâche. Mais nous voulons garantir que l'ordinateur produit finalement un résultat, et que ce résultat est celui que l'on veut.
Les savants ont décrit depuis l'antiquité des méthodes répétitives, des algorithmes, pour résoudre des problèmes précis. Par exemple, Euclide a décrit comment trouver le plus grand diviseur commun à deux nombres entiers (diviser le plus grand par le plus petit des deux nombres, recommencer avec le plus petit et le reste de la division, s'arrêter lorsque le reste vaut 0), et Héron d'Alexandrie comment calculer la racine carrée d'un nombre (faire la demi-somme d'une approximation et du nombre divisé par cette approximation, recommencer avec cette valeur comme nouvelle approximation, s'arrêter si c'est suffisamment proche). Par des raisonnements mathématiques, on peut montrer que ces méthodes qui bouclent progressent effectivement vers la résolution du problème.