Exercise 3: Why Formal Verification Beats Simply Re-Running the Program — Possible Solution
================================================================================================

Simply re-running Appel and Haken's original 1976 program again would
only confirm that the SAME software, on the SAME kind of hardware,
produces the SAME output as before. It wouldn't address the real,
underlying worry critics like Schmidt's later error discovery actually
confirmed was legitimate: that the original program itself, or the
larger informal argument surrounding it, might contain a genuine
mistake that a second run of the identical code would simply repeat
rather than catch.

Gonthier's real 2005 work is fundamentally different in kind, not just
in effort. Formally verifying the proof in Coq means translating the
ENTIRE mathematical argument - not just the case-checking computation,
but the surrounding logical structure connecting it to the actual
theorem - into a form that Coq's own kernel can independently check
against the basic, extremely well-scrutinized rules of formal logic
itself. This shifts what has to be trusted: instead of trusting Appel
and Haken's original, complex, custom-written case-checking program (and
every subsequent revision of it), you only need to trust Coq's own
much smaller, independently-verifiable kernel - a program simple
enough that its own correctness has been separately, heavily
scrutinized by the broader formal-methods community.

This matters because trusting a small, well-studied kernel is a
fundamentally more defensible position than trusting a large, bespoke
1970s program written specifically to solve this one problem - even if
re-running that original program a hundred more times kept producing
the identical result, none of those extra runs would actually reduce
the risk that a subtle bug was baked into the program's own design from
the start.

ANSWER: Re-running the original 1976 program would only confirm the
same code produces the same result again, without addressing whether
that code itself might contain a genuine bug (exactly what Schmidt's
later discovery showed was a real risk). Gonthier's formal verification
instead moves the entire proof into Coq, so that only Coq's own small,
independently-scrutinized kernel needs to be trusted - a fundamentally
smaller and more defensible trust requirement than relying on a large,
bespoke, one-off program.

WHY THIS WORKS AS AN ANSWER
------------------------------
This explains the real difference between repeating an unverified
process and independently re-deriving the same result through a
smaller, more trustworthy verification mechanism, tying it back to the
chapter's own real Schmidt-error finding as concrete evidence the
concern was legitimate.