Yes, but a C or Python program that “implements” a proof and which you test by running it on a few inputs is very different from a program in a interactive theo

Yes, but a C or Python program that “implements” a proof and which you test by running it on a few inputs is very different from a program in a interactive theorem prover like Rocq or Lean. In the latter, validity is essentially decided by type-checking, not execution