The Coq mailing list

["Marc Daumas" <Marc.Daumas AT ENS-Lyon.Fr>]

Dear colleagues,

I would like to raise the question of our liability in publishing proof
scripts on the Internet. The question is not new but it keeps re-surfacing
as UCITA is being discussed in the United States although UCITA only makes
things worse.

http://www.computerworld.com/softwaretopics/software/story/0,10801,81812,00.
html

Here is a quote from GNU's web site:

"You see, UCITA says that by default a software developer or distributor is
completely liable for flaws in a program; but it also allows a shrink-wrap
license to override the default. Sophisticated software companies that make
proprietary software will use shrink-wrap licenses to avoid liability
entirely. But amateurs, and self-employed contractors who develop software
for others, will be often be shafted because they didn't know about this
problem. And we free software developers won't have any reliable way to
avoid the problem."

http://www.gnu.org/philosophy/ucita.html

I would like to know if some people in the Coq community set up a policy
about publishing proof scripts on the Internet. Are there some licenses in
use. I believe our situation is worse than some other developers' situation
as one can easily imagine that we produce flawless codes and proofs.

Sincerely,

--
Marc Daumas - Charge de recherche au CNRS (LIP - ENS de Lyon)
mailto:Marc.Daumas AT ENS-Lyon.Fr
 - http://www.ens-lyon.fr/~daumas
PGP Key FP : 86C8 3DB3 7118 517A AA13  5707 D617 13D6 7510 D750
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 85 83 - Fax: (+33) 4 72 72 80 80