The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Any code analyzer, implementing a function from source code to non-source outputs of any kind, will need to operate on a representation of the code. The .vo file here would presumably qualify. The input buffers of a word count program might well qualify! Does mere use of an intermediate representation of the code in the computation of a non-code result constitute the creation of a derivative work? Is a word count report based on the analysis of source code a derivative work? I'm not knowledgeable about the case law, but I'd be astonished if the answer were yes. As long as no elements of the original are incorporated in the new work, I think one can make a strong case that the new work is not derivative, even if the output is the result of applying some function to the source code input. But, ..., I'd need to look at the issue with more care, and particularly at the case history. A separate issue to consider is whether one has *permission* to use the original code. If one produces a work in a way that requires use of an original work, and permission for such use is not granted, then there could be related problems, including ones related the ability to copyright an "output", whether derivative or not.

Interesting question.

On Tue, Jul 14, 2020 at 9:30 PM Maximilian Wuttke <mwuttke97 AT posteo.de> wrote:

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.