Celem sprawdzania poprawności jest zminimalizowanie zaufanej bazy obliczeniowej .
Dzięki sprawdzaniu poprawności ani kompilator, ani twierdzenie twierdzeń nie muszą być poprawne. Artykuł wskazuje na to na stronie 3:
Neither the compiler nor the prover need to be correct in order to be guaranteed to
detect incorrect compiler output. This is a significant advantage since the VCGen and
the proof checker are significantly simpler than the compiler and the prover.
Sprawdzanie poprawności to tylko kilka wierszy kodu i można je sprawdzić ręcznie pod kątem poprawności. W przeciwieństwie do tego automatyczny przyrząd, który działa dobrze, jest niezwykle złożony i mało prawdopodobne, aby był poprawny, chociaż przy dobrze przetestowanych i szeroko stosowanych dowodach błędy będą w skrajnych przypadkach, które mogą nie być łatwe do uruchomienia. Spójrz na 30k kod LOC C, który składa się na Lingeling , najnowocześniejszy solver SAT, aby zobaczyć, jak skomplikowane mogą być automatyczne dowody twierdzeń. Bez sprawdzania poprawności musiałbyś udowodnić, że ten dowód twierdzenia jest poprawny. To więcej niż możemy zrobić ekonomicznie w 2015 roku.