Correct. One way to think of it is that running the program produces a proof of the theorem. But since the program is guaranteed to terminate with a proof (sinc

Correct. One way to think of it is that running the program produces a proof of the theorem. But since the program is guaranteed to terminate with a proof (since all functions are total in Coq), why run it at all? Type checking is sufficient.