> Myślę że w praktyce w ogóle nie ma możliwości przeprowadzenia takiego
> dowodu, nawet dla mniejszych programów. Jak udowodnić, że w dowodzie
> nie ma błędu?

To jest akurat rzecz podstawowa: wystarczy pokazać, że każdy krok dowodu
wynika logicznie z tez dowiedzionych wcześniej, albo przyjętych przez nas
aksjomatów, w oparciu o uznawane przez nas reguły wnioskowania
(które uważamy za oczywiste).

Walidacja dowodu jest zabiegiem bardzo prostym -- z pewnością
o wiele prostszym, niż znalezienie dowodu.

Oczywiście pewien problem natury epistemicznej wiąże się ze sformułowaniem
odpowiedniej listy aksjomatów, które miałyby odzwierciedlać rozważany
przez nas problem