The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I don't understand this point. The specification for the correctness proof must have a model of the C code, even if you elide proof scripts and the proof itself. This model need not be a full representation (it only needs to capture the execution semantics, so it can certainly elide things like comments and the exact syntax used), but it needs to show up in the theorem statement.

Indeed, the correctness statement refers to the Gallina AST (of the C code) which is in a separate file, say code.v. The crucial part is that code.v need not be distributed: the client can download it themselves and then check the proof. 

Let me simplify and concretize the problem to get to the essence of my question:

(switching from C code to Gallina code)

Suppose we have a file code.v which contains some awesome Gallina function.

Suppose we have a file codeCorrect.v which contains a correctness proof of the function in code.v. Suppose this proof does not use any automation (just uses basic tactics like rewrite, apply, simpl)

Obviously codeCorrect.v Require Imports code.v

Should codeCorrect.v be considered a derivative of code.v?