Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Z3 theorem prover is now open source

research.microsoft.com

Post reply on HN
Print view View original

71–77 of 77 posts

Re: The Z3 theorem prover is now open source

#71

Post by sadga »

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 above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware.

MSFT claims a non-exclusive right to use your modifications.

Re: The Z3 theorem prover is now open source

#72

Post by subleq »

As a plain old programmer, would a tool like this be useful to me? How can I use a theorem prover to improve my code, or make it easier to write my code on a day to day basis? I've heard that Z3 is used for demonstrating security properties, how would I apply this to ensure my own systems are secure?

Re: The Z3 theorem prover is now open source

#73

Post by zvrba »

algorias wrote: post #60
zvrba wrote: post #58

People bitching about MS misusing the term "open-source" are, IMO, ungrateful SOBs who have never attempted to implement a non-trivial algorithm based on nothing but a stack of academic papers. For me, the greatest value in having the source is to learn from it, not to hijack it.

I think a lot of people appreciate the move MS made while simultaneously condemning them for their casual appropriation of a term having a well-established meaning. They've updated the blog post in the meantime, so this is a non-issue. Resorting to ad-hominems does nothing to strengthen your argument, btw.

Care to show some signs of appreciation by those who complain?

Re: The Z3 theorem prover is now open source

#75

Post by iy56 »

nitrogen wrote: post #48
iy56 wrote: post #45

Earlier quoted context omitted.

When you ask your officemate to open the window, does legal tell you to stop saying that Word(TM) because you're not using it according to the way Microsoft defined it?

No, but if I hypothetically created and started describing a graphical windowing system as a "Windows," and a word processor as a "Word," Microsoft would surely complain. It seems a bit hypocritical to complain about others' dilution of Microsoft's own marks, but then dilute others' marks in return. This is a bit of a digression from the original topic, but seems tangentially relevant given that we're talking about M…

Window managers are still commonly called window managers today. Word processors are still called word processors. That's the point - Microsoft hasn't taken away these generic terms. No, you can't call your competing product the exact same thing they call theirs. Why should you be able to? That'd be retarded.

Re: The Z3 theorem prover is now open source

#76

Post by nitrogen »

iy56 wrote: post #75
nitrogen wrote: post #48

Earlier quoted context omitted.

No, but if I hypothetically created and started describing a graphical windowing system as a "Windows," and a word processor as a "Word," Microsoft would surely complain. It seems a bit hypocritical to complain about others' dilution of Microsoft's own marks, but then dilute others' marks in return. This is a bit of a digression from the original topic, but seems tangentially relevant given that we're talking about M…

Window managers are still commonly called window managers today. Word processors are still called word processors. That's the point - Microsoft hasn't taken away these generic terms. No, you can't call your competing product the exact same thing they call theirs. Why should you be able to? That'd be retarded.

No, you can't call your competing product the exact same thing they call theirs.

Likewise, it is reasonable that Microsoft can't call their competing license "open source" when that term already has an established commercial definition and trademark with a specific set of consumer expectations.

Further, until a tradmeark is filed or established by extensive use, competing products can use similar words in their titles. Once upon a time you could have had Microsoft Windows, OpenWindows, the comp.windows.x newsgroup (suggesting that X is a subset of the generic category of "Windows"), etc. Now they will sue if your OS name even rhymes with Windows.

Re: The Z3 theorem prover is now open source

#77

Post by iy56 »

nitrogen wrote: post #76
iy56 wrote: post #75

Earlier quoted context omitted.

Window managers are still commonly called window managers today. Word processors are still called word processors. That's the point - Microsoft hasn't taken away these generic terms. No, you can't call your competing product the exact same thing they call theirs. Why should you be able to? That'd be retarded.

No, you can't call your competing product the exact same thing they call theirs. Likewise, it is reasonable that Microsoft can't call their competing license "open source" when that term already has an established commercial definition and trademark with a specific set of consumer expectations. Further, until a tradmeark is filed or established by extensive use, competing products can use similar words in their title…

Agreed. But that's all very general stuff. Nothing there so much as hints at special treatment for MS's trademarks specifically, which is what I was initially objecting to.
Post reply on HN