Entries:
Posts:

Something went wrong getting user information from Channel 9

Latest Achievement:

Something went wrong getting user information from MSDN

Visual Studio Achievements

Latest Achievement:

Something went wrong getting the Visual Studio Achievements

Bart De Smet: LINQ to Z3

Right click “Save as…”

Bart De Smet is one of the highly talented software engineers on Erik Meijer's team and the chief architect of the LINQ to Anything dream. You should watch his excellent PDC10 session on this topic.As you learned on Channel 9 Live's PDC10 conversation with Wolfram Schulte and Erik Meijer, Z3 is a theorem prover (the fastest in the world, in fact). Z3 is one of several advanced software engineering technologies coming out of MSR's RiSE team.

A while ago, Bart implemented a LINQ to Z3 library and I've wanted to dig into this with him for some time. Recently, I got the chance to do just that and it makes for an excellent episode of Going Deep.

Bart writes in his initial post on the LINQ to Z3 project:

With LINQ to Z3 my goal is to abstract away from the low-level Z3 APIs and provide nice syntax with rich static typing support on top of it. The basic idea is the following:

• Define the “shape” of a theorem, e.g. what symbolic names (and their types) to use;
• Express constraints over those symbolic names using LINQ syntax (more specifically the where keyword);
• Ask the resulting object for a solution, resulting in an instance of the “shape” type specified at the start.

An example of LINQ to Z3:

```var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
where t.X1 - t.X2 >= 1
where t.X1 - t.X2 <= 3
where t.X1 == (2 * t.X3) + t.X5
where t.X3 == t.X5
where t.X2 == 6 * t.X4
select t;
var solution = theorem.Solve();
Console.WriteLine("X1 = {0}, X2 = {1}, X3 = {2}, X4 = {3}, X5 = {4}", solution.X1, solution.X2, solution.X3, solution.X4, solution.X5);```

How does LINQ to Z3 work, exactly? Why did Bart do this? What is Z3 useful for? How does it work? Here, we get answers to all of these questions with lots of meaty whiteboarding and demo at the end of the conversation. As usual, there is a lot of information presented here and in a way that is readily understandable by non-experts - this is one of Bart's excellent traits: clearly explaining complex subjects so you don't have to be as smart as Bart to fully understand. I left Bart's office with better understanding of LINQ, Z3 and LINQ to Z3 (also Solver Foundation and Bart's definition of monad....). Thank you, Bart!

By the way, this is espisode 201 of Going Deep. Bart and LINQ were the focus for the 100th episode. It's nice to have this 100 episode cycle (LINQ to Anything is LINQ to Everything in this revolution). Thanks to all who have made this series truly interesting! Here's to 200 more.

Tune in.

Learn. Enjoy. Code.

Tags:

• Oops, something didn't work.

Getting "follow" information
• Yes! linq-to-z3 lives does this mean you're going to resume that blog series bart?

people who havent really needs to watch barts pdc talk, its pure awsomeness

• Here's the link to Bart's PDC10 session that requires Silverlight (the one I included in the description is a link to the WMV file for download): http://bit.ly/bfzKCk

C

• Oh yes, I've also wondered about the relation between Z3 and Solver Foundation. How they overlap, if one is the successor of the other or they are meant to be complementary.

Sum: (IEnumerable<T> | IObservable<T>) -> Maybe<T> such that result: Maybe<T> : IObservable<T> where result.Count() = 1  (Z3 constraint)

Maybe use IQbservable perhaps...

Watching rest after (incredibly long iPad iOS update ..)

Edit: On second thought: the obvious name for Maybe<T> is not Maybe<T> it's of course:

MaybeLater<T>!

• @exoteric: Good thinking, exo. LINQ to Solver Foundation is probably already on Bart's LINQ invention list.

C

• Someone needs to use L2Z3 and create a library of purity constraints so that any program can be analyzed for optimizability; next step of course to use those to simplify programs

Love the explanation of Sudoku base theory.

• i really really hope linq-2-z3 makes it out into a library that people can use

also, i wonder if you could use the "let" keyword to define z3 symbols instead of using the ghost type:

```from s in theoremcontext
let symbol1 = s.makesymbol<int>()
let symbol2 = s.makesymbol<int>()
where symbol1 > symbol2
select new {symbol1, symbol2};```

in might be problematic because the "T" in Theorem<T> is defined in the final select, if you dont include all the symbols youve declared in the query, they woudnt appear in the proof.. still, the syntax whould be pretty nice

• Very interesting!  My mind is spinning with crazy ideas about how to use this.

• LINM, yeah. but when you Linq to Everything, does those Standard Query Operators works smoothly for 'everything' ? and if customized operators can only be used as extension methods, this weakens the 'language intergrated' part. can Compier-as-a-Service help ?

and Z3 rules, cant wait to see it get its way into more places as the core infrastructure of system platforms.

• This sounds interesting, I'd love to watch it.

However, even the "Lo-band, Mobile" version is a 1GB download? You've got to be kidding...

• This sounds interesting, I'd love to watch it. However, even the "Lo-band, Mobile" version is a 1GB download? You've got to be kidding...

In fact, the MP4 for mobile file is 420MB... No kidding.
C

• The MS Dutch Mafia strikes again! :)

• The MS Dutch Mafia strikes again!

Bart is from the Kingdom of Belgium, technically

• Wicked cool. Keep up the great work!

• Great work, very cool!

• This is very nice.

But what I am really looking forward to is LIM to "compiler service" when it comes out. It's going to be pretty cool to compose run time generated programs. And something tells me this is what Bart is secretly working on since his blog post about LINQ to Z3 is from April 2009

• @Charles: Right, though Bart is probably from the Flemish (Dutch-speaking) part of Belgium. At least that is what I would guess due to his accent.

Great, inspiring interview, btw.

• @aL_: No commitments for a continuation (pun intended) of my blog series on the subject just yet. Expect an update after noodling around a bit more with Solver Foundation.

• @exoteric: A lot of real-world technologies already use Z3, cf. their portofolio mentioned in various presentations (see http://research.microsoft.com/en-us/um/redmond/projects/z3/documentation.html for some links, e.g. to the Slides for WING 2009, cf. slide number 4). But creative minds can of course go crazy using Z3, subject to its academic license that is (no, I'm not an attorney ).

Concerning Z3 versus Solver Foundation, I think the versus approach used for technology comparison is a little misplaced. Sure, there's some overlap, but Solver Foundation has its own strength and positioning in the market. Referring to it by its codename, "Optima", you should get some good insights in the kinds of problems it specifically aims to tackle. The target audience is also much further away from low-level software plumbers, more into the realm of business analysist (cf. its plug-in with Excel).

Once we make progress on (still hypothetical) Solver Foundation bridges using LINQ, I'll provide you with an update through the known channels .

• @aL_: Your idea of using let-bindings in query expressions is definitely worth looking at. In fact, I've done something along those lines before (I won't elaborate on the broader context there just yet, in order to whet the appetite of the Niners ). One drawback is its use of Select underneath (through compile-time erasure using transparent identifiers), which makes it indistinguishable from proper select clauses. Hence, we open the door for more expressive queries written by the user, for better or for worse. This said, some tricks can be played.

• @felix9: Standard Query Operators go only as far as what was once deemed "standard" and applicable to "queries". Monads are a superset of sequence-style query comprehensions.

Let's elaborate a bit on those points. First, even within the domain of querying, different data models or acquisition methods can give rise to other kinds of operators. For example, the push-based nature of IObservable<T> makes it a very natural candidate for signal-based programming where an observable sequence acts as a signal wire (e.g. TakeUntil). While it'd be very natural to expose such capabilities using language-integrated constructs, that may be a bit of a stretch as it goes beyond general purposing querying (which, till further notice, LINQ is about). Similarly, time-centric operators open up for a whole series of imaginary additions as well.

Personally, I do like the query comprehension syntax for the things it's good at. At some point, you'll for sure run short on the provided keywords (with varying mileage in C# versus VB, the latter of which has more keywords added for LINQ), but you can quite gradually "ease into" the dotting style of operator chaining (unless you have to insert between existing clauses, bad luck if you don't like some wholesale refactoring of the query expression).

Stricly speaking, you'd only need SelectMany (aka "bind") support ("do"-notation in Haskell, multiple from clauses in C#), to have all the power of monads at your service, assuming there are ways to "return" into the monad (e.g. new[] { value } for enumerables, Observable.Return for observables, etc.). Obviously that's too minimalistic (search for my project called MinLINQ to see this extremism in practice).

Finally, on the CaaS front, it's not at all sure at this point whether language syntax will be provided as an extensibility point, unless you can go in and extend the lexer and parser itself (causing you to create a new "dialect" of C#/VB altogether). Doing so definitely would limit the movements the benevolent dictators of the language design can take going forward ("oops, we may be clashing here with the 'bar' keyword introduced by customer 'foo' for the 'baz' dialect of C#"). The fluent nature of extension methods and the (relative, that is, without the support for "sectioning") conciseness of lambda expressions makes C# already a fairly good host for internal DSLs that follow an API-centric design. Popular patterns can always be lifted into proper language constructs, e.g. LINQ and the new "await" stuff.

• @Batman: @Charles: @Novox: The Flemish part it is indeed. For a good introduction into the many sub-atomic (due to the size) dimensions (due to regions, governments, languages, etc.) of the country Belgium, have a look at http://www.youtube.com/watch?v=QlwHotpl9DA (obviously they're wrong about the "Swiss chocolate" and "French fries" ).

I'm personally from the area around Ghent (visit using Bing maps: http://www.bing.com/maps/?v=2&cp=sh8826h998kx&lvl=18.21744759896361&dir=2.693629766958403&sty=b&where1=Ghent%2C%20Belgium&q=ghent), so my accent is definitely Dutch, though I speak a bit of French and German as well.

• @Kyrae: Some interesting thoughts you have there .

• [quote]
17 hours ago, Charles wrote
*snip*
Bart is from the Kingdom of Belgium, technically

[/quote]
His accent is very telling, he must be Flemish at least. Let's ask him: Hey Bart, are you Flemish?
:) :) :)

• @bdesmet: tease

i'd love to see more blog posts and c9 content on expressions trees and how you can bend them to your will in the context of linq providers and other things.. Expression<Func<T>> is one of those things that i have a feeling is extraordinarily powerful but that i just barely know how to handle, but one wrong step i'd come tumbling down

z3 is even further down those lines, it seems almost like witchcraft, you ask it anything and it just replies with an awnser that is garantueed to be correct. you "just" have to be sure you ask it the right question

• Currently watching the video and it's nice so far.

Also, when Bart used the word "aspect" in his explanation of what a monad is, I was reminded of the following paper: On the relation of aspects and monads.

• Bart, do you have any plans to update your blog post to reflect the changes to the managed Z3 API?

EDIT: i've managed to get a version of Bart's code to build/run against Z3 v2.15, but i don't think i can share it since i can't find a license on Bart's blog

• BTW, perhaps a further episode can do an interview with Z3 people about the inner workings of the algoritms of Z3. Perhaps that's a bit too deep, but it would be very interesting :)

• I have a friend who works on another SMT solver, (that's actually available under an open source license instead of the onerous MSR-LA terms), CVC3. Hmm, a LINQ provider for it might be an interesting project ...

• @piersh: I'll figure out a way to get the bits to the community in the forseeable future. Likely some further exploration is desired to streamline the experience further and have more Z3 constructs exposed through the API. Stay tuned.

• @aL_: Will see what we can do around this in the future. This said, expression trees are more of a tool than a destination. However, as more LINQ to Anything stuff materializes, I can see some good fit for a future episode that would benefit from further explanation of those animals.

• @bdesmet:

looking forward to it

• @bdesmet:great stuff indeed greetings from Italy