Entries:
Comments:
Posts:

Loading User Information from Channel 9

Something went wrong getting user information from Channel 9

Latest Achievement:

Loading User Information from MSDN

Something went wrong getting user information from MSDN

Visual Studio Achievements

Latest Achievement:

Loading Visual Studio Achievements

Something went wrong getting the Visual Studio Achievements

Bart De Smet: LINQ to Z3

Download

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:

Follow the Discussion

  • Allan LindqvistaL_ Kinect ftw

    Yes! linq-to-z3 lives Big Smile does this mean you're going to resume that blog series bart? Smiley

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

  • CharlesCharles Welcome Change

    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

    Get all the related download materials for Bart's talk at http://microsoftpdc.com

    C

     

     

  • Bent Rasmussenexoteric stuck in a loop, for a while

    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.

    I like using asynchrony for exiting the monad, in particular what about this:

    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 Sad ..)

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

    MaybeLater<T>! 

  • CharlesCharles Welcome Change

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

    C

  • Bent Rasmussenexoteric stuck in a loop, for a while

    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 Smiley

    Love the explanation of Sudoku base theory.

  • Allan LindqvistaL_ Kinect ftw

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

    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 Smiley

  • Richard Anthony HeinRichard.Hein Stay on Target

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

  • felix9felix9 the cat that walked by itself

    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.

  • meta-commentermeta-​commenter

    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...

  • CharlesCharles Welcome Change

    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

  • BatmanBatman

    The MS Dutch Mafia strikes again! :)

  • CharlesCharles Welcome Change

    The MS Dutch Mafia strikes again! Smiley

    Bart is from the Kingdom of Belgium, technically Smiley

  • Greg Braygbrayut Check out PhraseMeme Scanner for Windows Phone at ​PhraseMeme.​com

    Wicked cool. Keep up the great work!

  • JulesJules

    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 Smiley

  • NovoxNovox “Simplicity is the ultimate ​sophisticat​ion.” —Leonardo da Vinci

    @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.

  • Bart De Smetbdesmet Bart De Smet ​[MSFT::SQL::​Cloud​Programmabi​lity::Rx]

    @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.

  • Bart De Smetbdesmet Bart De Smet ​[MSFT::SQL::​Cloud​Programmabi​lity::Rx]

    @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 Wink).

    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 Wink.

  • Bart De Smetbdesmet Bart De Smet ​[MSFT::SQL::​Cloud​Programmabi​lity::Rx]

    @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 Wink). 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.

  • Bart De Smetbdesmet Bart De Smet ​[MSFT::SQL::​Cloud​Programmabi​lity::Rx]

    @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.

  • Bart De Smetbdesmet Bart De Smet ​[MSFT::SQL::​Cloud​Programmabi​lity::Rx]

    @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" Tongue Out).

    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.

  • Bart De Smetbdesmet Bart De Smet ​[MSFT::SQL::​Cloud​Programmabi​lity::Rx]

    @Kyrae: Some interesting thoughts you have there Smiley.

  • BatmanBatman

    [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?
    :) :) :)

  • BatmanBatman

    @Batman:Oops he already answered! hehe

  • Allan LindqvistaL_ Kinect ftw

    @bdesmet: tease Wink

    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 Tongue Out

     

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

    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 Sad

  • JulesJules

    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 ...

  • Bart De Smetbdesmet Bart De Smet ​[MSFT::SQL::​Cloud​Programmabi​lity::Rx]

    @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.

  • Bart De Smetbdesmet Bart De Smet ​[MSFT::SQL::​Cloud​Programmabi​lity::Rx]

    @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.

  • Allan LindqvistaL_ Kinect ftw

    @bdesmet:

    looking forward to it Smiley

  • @bdesmet:great stuff indeed greetings from Italy Smiley

Remove this comment

Remove this thread

close

Comments Closed

Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation, please create a new thread in our Forums,
or Contact Us and let us know.