The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

On 15/07/2020 03:03, Abhishek Anand wrote:
> Well, the issue here is more complex, because the proof must contain
> the full representation of the C code
> (I said "must" but I have no proof of such statement, and I would love
> to be shown wrong)
> 
> 
> Highly automated proofs often do not contain the representation of the
> code. The Ltac proof scripts are often just algorithms that find the
> concrete proof, when applied to the concrete Coq AST representation of
> the C code, the latter need not be distributed with the Ltac proof scripts. 

Assume that you can re-use your proof script to certify different
(possibly annotated) C code also. Then, I think, your proof script is
more like a 'compiler' -- an independent tool -- rather than a derived work.

However, at the end, the .vo file will contain some representation of
the AST -- at least in the type of the correctness lemma. I would argue
that the .vo file would be a derived work then. However, the .vo file
need not to be distributed.