Commercial licenses were previously $10000! Also, this makes the open sourcing of projects which depend on Z3 (like F*) much more valuable.
what is the “F*” project? I’m having trouble searching for it …
It’s a dependently typed programming language / verification tool, somewhat in the vein of Agda: https://fstar-lang.org/
Wow, Microsoft is really investing in Open Source: ASP.net, Halo engine, now this…
Not sure what to make of it. I have a nagging feeling its a marketing ploy.
I doubt this is a marketing ‘ploy’. Z3 is an extremely versatile solver, and once industry applications start using Z3 in their products, Microsoft will gain a huge amount of good will. Also Z3 itself is pretty much written and maintained by a single guy in Microsoft, and having more eyes on the code will be a big boon. Recently, a bug was found in the Coq proof engine, and I’ll bet it would be nice if we were more confident that Z3 will not have similar errors.
I wouldn’t count on Z3 being less buggy than Coq. If there’s a formal verification of Z3 itself, I can’t find it in my first skimming of the source code. Also, my personal experience with Z3 is that while it’s very good and could not be fairly called unstable, it’s also not defect-free. Then again, Z3 and Coq do different things anyway.
The “falso” bug/satire was really funny, but I don’t think it will lead to a massive exodus from Coq.
Microsoft has (quietly, almost secretly) sold Z3 commercially for some time, but I doubt it’s funded MSR. It’s entirely possible that cold business analysis shows that free Z3 adds more to the bottom line than $10K Z3. If that’s a marketing “ploy,” I’ll take it!
My personal hope for Z3 is we’ll see a bunch of new languages that, similar to F*, use the solver to help programmers write code which is both more correct and more optimized. We’ll see!
Here is an example of Z3 bug in the wild that was found while developing a superoptimizer for LLVM: http://blog.regehr.org/archives/1192
The scary thing is that this is an off-by-one bug. Be sure to check the diff of the fix. The comforting thing is that there are multiple SMT solvers and the standard input/output format, and the bug was found by crosschecking with other solvers. Although Z3 is by far the best solver, you absolutely should check Z3 against other solvers.
It worries/excites me to see Microsoft releasing more of its Microsoft Research. I like seeing the awesome stuff they’ve been working on, but worry that they are seeing open source as an alternative to having incredible research labs like the Silicon Valley one they closed last year.
Great news! Hopefully a nod for programming language hobbyists to experiment with it, I certainly will (in a possibly far future …)