The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Wed, 15 Jul 2020 23:12:37 -0400
Stefan Monnier <monnier AT iro.umontreal.ca> wrote:

> >> Another approach would be to ask the owner of the C code whether
> >> they have any objection to your publishing the proof.  Seems to me
> >> your proving it would make their code more valuable.  
> > The C code is available publically under GPLv2 license. The main
> > question is whether the correctness proof (just the .v file(s)
> > containing the specs and proofs, NOT the code or the .v file
> > containing the code AST) can be released under a different license
> > (possibly incompatible with GPLv2).  
> 
> I'm not sure what there could be to gain from using an incompatible
> license, but Jim's approach is still relevant anyway: ask the
> author(s). If they're OK with it, then you don't need to figure out
> what the law says.
> 
> 
>         Stefan
> 

If someone is eventually able to generate code based on the proofs in
the .v file that performs the same function as the original code, and
the .v file is not itself considered a derivative work (even if by
virtue of the author agreeing to that effect), then does the ability of
the original GPLv2 to protect derivative works of the original code
disappear?