GoingDeep: Bart De Smet: LINQ to Z3

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.