The Z3 theorem prover is now open source • Hacker News Board

Re: The Z3 theorem prover is now open source

#11

Post by frabcus » Wed, Oct 03, 2012, 8:29 AM UTC

lucian1900 wrote: post #8

gojomo wrote: post #2

The limitation to non-commercial use means it's not quite 'open source' in the common meaning established by the Open Source Initiative. (Discrimination against a 'field of endeavor', such as business use, is not allowable under their definition.)

It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.

Thanks both for pointing this out - I've left a comment on the blog post asking him to change "open source" to "shared source" (which is what I thought Microsoft call such visible but not open code).

I'll give Leonardo the benefit of the doubt that he's just made an error for now...

Re: The Z3 theorem prover is now open source

#12

Post by seanmcdirmid » Wed, Oct 03, 2012, 8:31 AM UTC

lucian1900 wrote: post #8

gojomo wrote: post #2

The limitation to non-commercial use means it's not quite 'open source' in the common meaning established by the Open Source Initiative. (Discrimination against a 'field of endeavor', such as business use, is not allowable under their definition.)

It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.

Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation.

Full disclosure, I work for Microsoft.

Re: The Z3 theorem prover is now open source

#13

Post by wladimir » Wed, Oct 03, 2012, 8:32 AM UTC

praptak wrote: post #9

wladimir wrote: post #6

Earlier quoted context omitted.

IMO it's still exciting. Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from. And it means that it can be ported to platforms it's currently not available for.

> Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from. As long as nobody sees you, otherwise you are vulnerable to a lawsuit. If I had serious plans to make my own implementation I would purposefully avoid even running this program.

Right, if you intend to make your own implementation and profit from it, it's wise to avoid it. But for the rest of us it isn't that black and white...

Re: The Z3 theorem prover is now open source

#14

Post by throwaway64 » Wed, Oct 03, 2012, 8:46 AM UTC

seanmcdirmid wrote: post #12

lucian1900 wrote: post #8

Earlier quoted context omitted.

It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.

Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation. Full disclosure, I work for Microsoft.

Open Source a term with a single, specific definition.

It is damaging to the ideas of FLOSS to allow stuff like "shared source" to be called open source.

EDIT: Removed reference to "open source" being trademarked, it is in fact not, apologies for the confusion.

Re: The Z3 theorem prover is now open source

#15

Post by wiradikusuma » Wed, Oct 03, 2012, 8:50 AM UTC

ot wrote: post #4

This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it! Some context, as not everybody may have heard about it. Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver. You can play with it online using its Lisp-l…

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

Re: The Z3 theorem prover is now open source

#16

Post by hermanhermitage » Wed, Oct 03, 2012, 8:57 AM UTC

throwaway64 wrote: post #14

seanmcdirmid wrote: post #12

Earlier quoted context omitted.

Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation. Full disclosure, I work for Microsoft.

Open Source a term with a single, specific definition. It is damaging to the ideas of FLOSS to allow stuff like "shared source" to be called open source. EDIT: Removed reference to "open source" being trademarked, it is in fact not, apologies for the confusion.

No. This is a fantasy.

A trademark does not take ownership of general words or phrases from the people.

Re: The Z3 theorem prover is now open source

#17

Post by andrewaylett » Wed, Oct 03, 2012, 9:05 AM UTC

derleth wrote: post #10

From the license text: > Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose. The above I…

The feedback thing is probably along the lines of not wanting to have to have internal controls to deal with confidential information in their feedback processing.

Re: The Z3 theorem prover is now open source

#18

Post by lucian1900 » Wed, Oct 03, 2012, 9:08 AM UTC

seanmcdirmid wrote: post #12

lucian1900 wrote: post #8

Earlier quoted context omitted.

It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.

Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation. Full disclosure, I work for Microsoft.

Microsoft trying to hijack a term with an already fully established meaning is dishonest and screws up everything. This may be an honest mistake by an employee that fell for Microsoft's own marketing, but it's still not right to spread misinformation. Is the license on this list [1]? Then it's almost certainly not open source. Also, this particular license has already been rejected by OSI.

The GPL is not the only open source license. It may screw up certain commercial usage, but it never stops users from forking the software. This Microsoft license does.

1. http://opensource.org/

Re: The Z3 theorem prover is now open source

#19

Post by skrebbel » Wed, Oct 03, 2012, 9:12 AM UTC

hermanhermitage wrote: post #16

throwaway64 wrote: post #14

Earlier quoted context omitted.

Open Source a term with a single, specific definition. It is damaging to the ideas of FLOSS to allow stuff like "shared source" to be called open source. EDIT: Removed reference to "open source" being trademarked, it is in fact not, apologies for the confusion.

No. This is a fantasy. A trademark does not take ownership of general words or phrases from the people.

Correct. A trademark is just that: a mark used in trade. It does not come with the ability to define a standard definition for the mark's meaning, other than "~ is a trademark of $ORGANISATION".

Also, is "open source" really trademarked? Wtf? That's like a beef promo organisation trademarking "well done".

Re: The Z3 theorem prover is now open source

#20

Post by throwaway64 » Wed, Oct 03, 2012, 9:13 AM UTC

hermanhermitage wrote: post #16

throwaway64 wrote: post #14

Earlier quoted context omitted.

Open Source a term with a single, specific definition. It is damaging to the ideas of FLOSS to allow stuff like "shared source" to be called open source. EDIT: Removed reference to "open source" being trademarked, it is in fact not, apologies for the confusion.

No. This is a fantasy. A trademark does not take ownership of general words or phrases from the people.

The problem with this idea when applied to this case is the motivations of people wishing to use some alternate definition. There is a real profit motive in being able to call stuff "open source" when it doesn't grant its users the same kind of freedoms the BSD or the GPL license, etc, do.

If you allow stuff like "shared source" to be called open source, you reduce the term to a meaningless buzzword, like how the term "open" is frequently abused.

citing trademarks is a heavy handed approach, but many parties with a profit motive don't care about anything except strict legality.

This is relevant in particular to this blog because Microsoft has a history of attempting to change what the term means

http://opensource.org/node/280