It is not trivial to separate commercial and non-commercial purposes. Creative commons licenses still don't have a clear criteria. So as it goes with copyright, this just has a chilling effect on the education of some compsci fundamentals. I just dont get why MS would do that, is it a competitive advantage?
Even then, if the teacher makes the text available to the students via a public web site, then its availability to non-students puts it outside of fair use.
However, the Z3 license does not prohibit teaching in general. In fact, it says:
"You may use, copy, reproduce, and distribute this Software for any non-commercial purpose, subject to the restrictions in this MSR-LA. Some purposes which can be non-commercial are teaching, academic research, public demonstrations and personal experimentation. You may also distribute this Software with books or other teaching materials, or publish the Software on websites, that are intended to teach the use of the Software for academic or other non-commercial purposes."
How does this have "a chilling effect on the education of some compsci fundamentals"?
If the software is going to be used for commercial purposes, then Microsoft wants some of the action. If you're going to teach how to use the software for commercial purposes, then Microsoft still wants some of the action.
(In case the sarcasm was a bit too thick, although it was at no less a level than your reply, I think it's plainly obvious what the licence is dictating and hope you will go into a little more detail of your viewpoint that it isn't)
Non-commercial use for something that is directly involved in the production of something else is fairly easy to determine; it depends on whether that something else is sold for money or not.
But for analytical software like this prover, you could indirectly use it to improve something that is sold for money, but the process of improvement is not necessarily a commercial transaction. It could be performed by students at a university, for example. I have in mind formal verification of program invariants, with potential identification of breaks, as an example.
Using your process of improvement for me it is quite clear there would be.
[Perhaps the solver could be used to figure the applicability of the licence]
False. There are cases where commercial was held to mean "any use by a for profit company, regardless if the use is research, earns money directly or indirectly", etc.
Although if you speak to a lawyer I'm sure their training would immediately start highlighting this as a concern I don't believe it should be in the vast majority of cases. Wasn't there an article on HN a few days ago basically summarising this type of concern under "so sue me" (minus expletives)
So if I use a software package commercially and don't pay for it perhaps the maximum I could be sued for in the local courts would be the license fee I didn't pay. If there is no "commercial" license then could it really be said that a loss has been suffered?
[NB I know contracts and licenses usually have clauses stating the jurisdiction where disputes will be resolved]
Non-commercial is a terrible term, because it's simply too vague. You can simply say "well, MS will use a bit of discretion, and not sue someone for a marginal infringement". But it does feel a little dodgy.