nEUrOO (./72) :

Lionel Debroux (./65) :
mais absolument pas de prouver qu'un programme est correct

C'est impossible: halting problem

euh, le problème de l'arrêt ne pose problème que dans les cas "difficiles"/ambigus : quand on a un logiciel critique on essaye justement d'être le plus clair possible et de s'en tenir à des invariants vérifiables facilement... et comme dit moumou ça marche très bien en pratique ^^

dualmoo (./77) :
en pratique ça prouve l'airbus A380

oui enfin prouver l'absence d'exceptions c'est quand même loin d'être "prouver la correction" hein c'est juste "prouver que les autres preuves de correction sur le code ont effectivement un sens, i.e. qu'on ne viole pas la type-safety et qu'on a pas d'overflow"...