[mizar] Fwd: Fwd: License for MML

[Josef Urban <josef.urban@gmail.com>]

---------- Forwarded message ----------
From: "David A. Wheeler" <dwheeler@dwheeler.com>
Date: Sun, 21 Feb 2010 21:34:49 -0500 (EST)
Subject: Re: Fwd: License for MML (xyzzy)
To: josef.urban@gmail.com

> From: Josef Urban <josef.urban@gmail.com>
> Date: Sun, Feb 21, 2010 at 6:09 PM
> Subject: Fwd: License for MML

> Dear all,
>
> here is a sort of RFC on the licensing for Mizar Mathematical Library
> sent today to the Mizar mailing list. I am also forwarding it to a
> selected list of people who are probably not on the Mizar forum (you
> would have to register to post there, but I'll be happy to forward
> your replies there).
>
> I'll be grateful for your comments.

Thanks for forwarding this to me.  Here are my comments; if you could
forward them, I'd greatly appreciate it.

============

First, thanks for trying to work out good licensing and submission rules.
I started the Open proofs project (http://www.openproofs.org), and one
problem we're repeatedly having is that people do not make clear statements
about licensing.  As a result, a lot of work is unusable and must be ignored.

There is absolutely *no* need to have a "transfer of copyright" to have useful
submissions.   There are pros and cons to transfer of copyright:
* Plus: Transferring copyright *does* make it easy to do a mass
relicense of the work.
* Minus: Transferring copyright will make many authors unwilling or unable
   to contribute.  For example, many U.S. government employees and
some contractors
   will NOT be able to transfer copyright legally.  Even when they can, the
   paperwork may be more than they're willing to bear.  Many authors will be
   rightfully nervous about copyright transfers, for example, if the
organization
   "disappears", there's nothing that can be done to repair things.
   You can *partly* solve this by creating a formal organization (incorporate
   with by-laws, board of directors, etc.), but that kind of heavy organization
   has its own problems.
A common reason to require transfer of copyright is to create proprietary works,
but since I don't think that's the point of MML, that reason doesn't apply.

Most projects leave the copyrights with the authors
and merely require that the work be released under suitable licenses.
I suspect that would best suit MML, as long as you agree on a minimal set of
licenses for MML submission.  So, you just need to pick on a minimal
set of licenses.

One additional complication:  the Curry&#8211;Howard correspondence
shows that there is a direct relationship between computer programs and proofs,
but the law doesn't know about that; the law still thinks that
programs and proofs
are unrelated.  Thus, even though you may be *thinking* that you are
"writing proofs" (CC-BY-SA), some people may use those proofs to prove or write
programs, suddenly moving into the software world!!  So ideally, your
licenses would be appropriate to *both* worlds.

So, what license(s) do you pick?  There are various options, but let me at least
recommend a set of requirements.  The most common licenses by *far* for
community-developed materials are:
* CC-BY-SA for non-software (GNU FDL is probably #2, but diminishing)
* GNU GPL for software (more than 50%; others common ones are LGPL,
BSD-new, and MIT).

That doesn't mean you have to use those two licenses, but I believe it
is critically
important that whatever license(s) you choose are compatible with those two
(for their respective domains).  Options include:
* Dual licensing with both CC-BY-SA and the GNU GPL (version 2 or
greater), if you wanted to require by law that further contributions
be shared.
* Dual licensing CC-BY-SA and GNU LGPL (version 2 or greater)
* BSD-new (http://www.opensource.org/licenses/bsd-license.php).  That
can be combined with CC-BY-SA, GPL GNU, and many others.

For more discussion on licensing, you might want to look here:
http://www.dwheeler.com/essays/gpl-compatible.html

I wish you well!!

--- David A. Wheeler