Stream: coq-community devs & users

Topic: What are the preferred open source licenses?


view this post on Zulip Bas Spitters (Jun 07 2020 at 07:49):

Does the community prefer MIT over LGPL ?

view this post on Zulip Karl Palmskog (Jun 07 2020 at 09:42):

@Bas Spitters looking at the repositories on GitHub, I would argue the community favors permissive licenses like CECILL-B, MIT, BSD, Apache-2.0, although a precise figure would require scripting/mining. Older work often follows Coq and uses LGPL.

view this post on Zulip Karl Palmskog (Jun 07 2020 at 10:04):

permissive licenses are great for maximizing reuse of a project --- see, e.g., Richard Stallman's explanation for why he endorsed licensing the Vorbis codec under BSD: https://lwn.net/2001/0301/a/rms-ov-license.php3

view this post on Zulip Karl Palmskog (Jun 07 2020 at 10:22):

did a simple search via GitHub (which doesn't allow selecting CECILL-B/CECILL-C):

view this post on Zulip Gaëtan Gilbert (Jun 07 2020 at 10:32):

e.g., Richard Stallman's explanation for why he endorsed licensing the Vorbis codec under BSD: https://lwn.net/2001/0301/a/rms-ov-license.php3

The patent concerns were pretty influencial there

view this post on Zulip Karl Palmskog (Jun 07 2020 at 10:47):

since most Coq projects are directly or indirectly funded by European or US tax money, there is also an argument that the results should be made available in a way that maximizes immediate reuse (benefit to the public), rather than "maximizing freedom" in some abstract, long-term sense.

view this post on Zulip Bas Spitters (Jun 07 2020 at 11:50):

Thanks for the overview! That's an interesting argument. Is there a more precise statement along those lines?
I'm aware of the push for open access/open data, but I believe that's agnostic about which open license one uses.

view this post on Zulip Karl Palmskog (Jun 07 2020 at 12:10):

the main difference to open access / open data is, in my mind, that publications and datasets are not often directly modified or integrated into derivative works (and software often is). So whether one uses permissive (MIT) or copyleft (GPL,CC-ShareAlike) for publications/data doesn't matter all that much, in my mind -- as long as the basic "openness" is there

view this post on Zulip Karl Palmskog (Jun 07 2020 at 12:12):

the FreeBSD project has some basic recommendations about when permissive licenses are applicable (https://www.freebsd.org/doc/en_US.ISO8859-1/articles/bsdl-gpl/article.html#recommendations):

The BSD license is preferable for transferring research results in a way that will widely be deployed and most benefit an economy. As such, research funding agencies, such as the NSF, ONR and DARPA, should encourage in the earliest phases of funded research projects, the adoption of BSD style licenses for software, data, results, and open hardware

view this post on Zulip Théo Zimmermann (Jun 07 2020 at 12:37):

I personally agree with the recommendation of using permissive licenses for output of publicly-funded research.

view this post on Zulip Théo Zimmermann (Jun 07 2020 at 12:39):

I've also explained previously why I'm against the use of LGPL for Coq libraries: https://github.com/coq-community/templates/issues/34#issuecomment-634565291

view this post on Zulip Théo Zimmermann (Jun 07 2020 at 12:40):

(But when it is tools and not libraries, I think that the GPL license is less problematic.)

view this post on Zulip Karl Palmskog (Jun 07 2020 at 13:46):

right, I think there is some sort of "hierarchy of usefulness of permissive licenses", going from least useful to most useful, with: datasets < tools < libraries

view this post on Zulip Gaëtan Gilbert (Jun 07 2020 at 13:48):

The same order could also be called a hierarchy of usefulness of copyleft licenses for the same reasons

view this post on Zulip Karl Palmskog (Jun 07 2020 at 13:51):

I think the difference is in what is meant by "useful". I meant "useful" here as "immediately useful to society [and thus also for economical activity]" and there is also "useful" in the sense of Stallman/FSF, which is something like "useful for furthering the goals of software freedom in the long run [even if to the detriment of being immediately useful for society]"

view this post on Zulip Karl Palmskog (Jun 07 2020 at 14:21):

I argue, from a "public welfare" standpoint, that publicly-funded research efforts should aim for the former and not the latter notion of usefulness

view this post on Zulip Karl Palmskog (Jun 07 2020 at 14:24):

the basic line of argument is that tax money going to research deprives the current members of the public from the possibility of (some measure of) consumption/welfare. Hence, we should aim to increase welfare for current members with research output when possible, and not merely be content with the possibility of enhancing the welfare of future members of the public

view this post on Zulip Karl Palmskog (Jun 07 2020 at 14:38):

it's a very common political strategy to justify public spending on efforts not in the general interest by claiming that that they will still benefit everyone in the long run. In these cases, it's warranted to be skeptical and scrutinize whether these benefits are even likely to materialize, and in particular what the "long run" can be expected to be. If the "long run" is far off, current members of the public are essentially taking one for the team, which I think is a serious agent problem (moral hazard) [assuming a government actually is de jure expected to uphold/improve the welfare of the current general public].

view this post on Zulip Karl Palmskog (Jun 07 2020 at 15:10):

regardless of what one thinks about FSF/Stallman/GPL (and I'm not against them in general), it's hard to argue that the following fact from the final paragraph of GPL2/GPL3 is conducive to immediate welfare-enhancement:

The GNU General Public License does not permit incorporating your program into proprietary programs.

view this post on Zulip Yishuai Li (Jun 08 2020 at 18:27):

The question becomes: Do proprietary programs necessarily benefit the general public?

view this post on Zulip Yishuai Li (Jun 08 2020 at 18:31):

IIUC GPL does permit commercial use of licensed programs, the key point is to make sure that all derivatives are accessible to the general public.

view this post on Zulip Karl Palmskog (Jun 08 2020 at 18:33):

in the short term, I think it's quite clear that not having license encumbrances to including code by researchers into your software benefits the public --- everyone can just copy it in and go on their merry way, whether proprietary or not

view this post on Zulip Karl Palmskog (Jun 08 2020 at 18:36):

you can argue like Stallman does that in the long term, having "locked-in" proprietary code does not benefit the public. But it's a large leap for governments to take that argument at face value (in the end, it's an empirical statement of uncertain status), and "bet" lots of tax money on it, which could mean depriving many of the benefits of their own forcibly-taken tax money/ welfare

view this post on Zulip Karl Palmskog (Jun 09 2020 at 11:49):

I guess this is turning more into in an essay, maybe I'll just post it on the Discourse as "opinion: publicly-funded Coq-related projects should use permissive open source licenses"

view this post on Zulip Yishuai Li (Jun 11 2020 at 17:02):

MATLAB is excluding users based on affiliation, targetting a specific nation. Yes this is violating free market rather than violating free license, but free software like SciLab doesn't involve such issue at all.
Question: Who is "the general public"?

view this post on Zulip Karl Palmskog (Jun 11 2020 at 17:09):

most research projects are funded by national or regional research agencies, e.g., in France or by the EU. For example, in France, the general public are French citizens and residents, and to the EU, the general public are citizens and residents of EU-member countries. My argument is based on the usual/common view in Europe and the US that nation states have obligations to the citizens and residents they tax. Since permissive licenses don't make distinctions on nationality or residence, the benefits become globally available, but this is a side-effect rather than the primary goal (which in this case is to provide reciprocal benefits to the taxed public of a specific country/area).

view this post on Zulip Pierre-Marie Pédrot (Jun 11 2020 at 17:16):

@Yishuai Li I am not sure what the "free market" is doing there at all, as far as I know states are still sovereign and they can BTFO international treaties because laws have precedence over them. If I were a Chinese citizen, the solution would be pretty straightforward, i.e. boycotting this kind of software and developping free alternatives

view this post on Zulip Yishuai Li (Jun 11 2020 at 17:23):

Is it still worth licensing a software if laws have precedence over the licence?

view this post on Zulip Pierre-Marie Pédrot (Jun 11 2020 at 17:24):

Insofar as it contextually makes sense, yes

view this post on Zulip Pierre-Marie Pédrot (Jun 11 2020 at 17:24):

I love the WTFPL FAQ about its difference with public domain for instance

view this post on Zulip Pierre-Marie Pédrot (Jun 11 2020 at 17:26):

Quoting it:

Isn’t this license basically public domain?

There is no such thing as “putting a work in the public domain”, you America-centered, Commonwealth-biased individual. Public domain varies with the jurisdictions, and it is in some places debatable whether someone who has not been dead for the last seventy years is entitled to put his own work in the public domain.

view this post on Zulip Alexander Gryzlov (Jun 11 2020 at 21:56):

There already exists a free alternative to Matlab: https://www.gnu.org/software/octave/


Last updated: Jun 03 2023 at 18:01 UTC