The Coq mailing list

[Izzy Hasson <izzyjhasson AT gmail.com>]

The issue with the question of whether a proof of correctness of C code is considered a derivative of the code from an IP/licensing/legal perspective is kind of incomplete. There are three sets of laws, I can think of, in the US that could be relevant, Patent, Copyright, and Contract, and each can yield different conclusions. With Patents ,assuming the code somehow had a valid patent attached to it, I can't imagine how the proof of code would be considered a derivative of the code and I don't think whether or not the proof contained a verbatim reproduction of the code would matter. With Copyright I can't think of how the proof of code wouldn't be a derivative of the code but you have fair use considerations which could render the question of derivation irrelevant. Finally with Contract law I have no clue.

Sincerely,

Some guy who is definitely NOT a lawyer