>> That was awesome. You got it? Cool.
I was going to give you more time to do
that. I need to pull up the program, so
I can talk to you. Sorry. Yeah! Okay.
Hi. I'm back. So... Guillaume is going
to talk to us next, and run us through
"The terrible Yook monster! Slayed by the
grandson of Master Prolog!"

(applause)

 >> This is the Yook monster. He's
pretending to be a villager. It doesn't
work very well, but if I put on my best
Zelda narrator voice, I held my sword in
the front, I pushed the doors open,
ready to hack and slash. To my shock,
all the villagers looked the same, and
each had something to say about the
other Anouki. FoFo said that you go mo
was honest. Kumu said Mazo or Aroo was
lying... (on screen)

Only the monster would lie. I can either
kill them all and let God sort them, or
try to think this through. Now... If I'm
going to try to think this through,
which programming language should I use?
Should I use maybe a programming
language that is machine inspired? That
is expressing its inner Turing
machine-ness, something that has as its
main defining abstraction the step? And
the ruthless destruction of the content
of a memory cell? Or maybe should I use
something a little bit more functional?
Such as purely functional Chris
Okasaki... Whose main defining
abstractions are functions, of course,
and function composition. In particular,
input-output-style function composition,
where you code a function, you get an
output. You call a function, you get an
output. On and on and on and on and on.
Well, I would advance of course that
this is a small silly logic puzzle, and
so we should kill this mosquito of a
logic puzzle with a bazooka of a
programming language, Alloy. We're going to use
a descendant of OCL, B, VDM, FDR, Z (also known
as "modeling" or "searching" programming
languages) and all decendants of
Grand Master Prolog. The
defining abstraction is the relation.
That brings you back to high school. The
days when you would learned that a
function is an association of a pair of
input and output, and if you want to
have two different output for the same
input, that's okay. You call it a
relation and you move on. But it does
mean that it becomes legit to ask: I
have this output, what is the input that
corresponds with it? In comparison, the
functional programming languages are
missing out. And the second defining
abstraction is our good friends
from mathematics, universal and existential
quantification. Now, to put that into a
wholly programmer's perspective of what
these two are, I'm going to say they're
a little bit like a for-loop that loops
over all things in the universe.

And you would tell me... Guillaume,
that's impossible. You know this. And
I'm going to tell you that's exactly the
same thing that they said about garbage
collection before it was invented! 
Before careful programming
language design made it possible. And so
in logic programming, the design of the
programming language will take over...
Check this out. This is an
exclamation mark put into the form of a
slide. Ptuh! It becomes the
responsibility of the programming
language to find time efficient bounds
for loops. Okay?

Whoa. I have over here the IDE for the
programming language Alloy. We're going to be
defining a sig, Anouki. A class, Anouki.
Anoukis exist, and they can be either
truthful or not. I have six Anouki. They
all extend Anouki, and then I have a few
facts to say about the relationship. If
FoFo said true, then GoMo is true.
If Kumu tells the truth, either one of
these tell the truth, and so on and so
forth. And I also known -- that's part of
the problem -- that there is only one
that is lying.

 >> Can you move to the left, please?
Thank you.

 >> Now, this is a little bit like awk.
You know how awk, you get that free loop
that goes over all the lines of the
input? Imagine here that this is a free
loop around all of this code that goes
over all of the possible items of the
universe. Now, here there's only six of
them. Who can be lying? So I press
control E. It loops over all the
possibilities, find the one that abides
to the facts. Aroo! Aroo is lying!

All right. Second example. I'm going to
introduce the second example with a
song. Called I'm My Own Grandpa.

 >> My father fell in love with her and
soon they too were wed. This made my dad
my son-in-law, and really changed my
life. Now my daughter was my mother...

 >> This is complicated.

 >> Was of course my stepmother.
Father's wife that... Makes me blue...
Because although she is my wife, she's
my grandmother too. Now, if my wife is
my grandmother, I'm her grandchild. And
every time I think of it, it nearly
drives me wild. Because now I have the
strangest case you ever saw. As husband
of my grandmother, I am my own grandpa.

How can this be possible? Let's ask Alloy.
I have a person who has a father and a
mother. Maybe not. A man is a person who
has a wife (This is pre-marriage equality.) A
woman has a person who has a husband.
Fact of biology. There is no person who
is in the transitive closure of their
mother and father relationship. You
can't biologically be your own father.
Terminology, wife is the reverse
relationship of husband. Social
convention. The mother/father
relationship, transitive closure, all
my ancestors. There is no wife and
husband relationship in my ancestors.
There is no incest. Good!

Grandpa... Grandpa is... Well, let's say
parent-parent is my mother, or my
father, or the relationship, which is
the composed relationship of mother,
composed with husband. My stepfather. Or
the wife of my father, my stepmother,
and a grandpa is my parent and my
parent, intersected with the set of all
men. My own grandpa is... A man, p, who
is in the set of his own grandpas. How
can this be possible? Oh! There is a
solution with four people. The song
needlessly makes things complicated! And
Alloy finds the simplest solution. If it
finds more, it shows you the simplest
solution first. In this case, I have a
man who is married to a widow, who has a
son. So he has a stepson, who marries
his mother. So backward... The man, his
mom, his stepfather, the grandmother,
the step grandfather, is his own
grandpa.

(applause) and we can show that
stepfatherhood, stepmotherhood, is
crucial to making this happen. Because
if I redefine parenthood without the
steps, and I say enumerate over a universe
with 60 people...

Pause for effect. No instance found!
What has just happened? There are 30
ways of choosing a father, 30 ways of
choosing a mother, 30 ways of choosing a
husband or a wife, one possibility for
not having each of these things. We have just
integrated over 10^164 permutations per
second. I have a 2.7gigahertz CPU. We
did 10^145 permutation instance-check
per clock cycle, one googol's worth of
checking. I have either the world's
fastest GPU, or Alloy is very clever about
its compilation strategy. It does not go to
bytecode. It does not go to assembly. It
goes to SAT. It compiles to SAT. SAT of
course is one of the foundational
problems in computer science. The first
problem to be identified as an NP
complete problem. Of course, since the
1960s, a humongous amount of effort has
gone into making SAT-solving software as fast as
possible. And so Alloy uses 55 years of
research in finding good search bounds.
That's why it is so amazingly fast.

Though we've used it to do logic problems in
the book by Daniel Jackson, at MIT, what
this is used for is to find bugs in
programs before you even begin writing
them. This is not a proof checker. This
is a proof breaker! that will find
problems before you begin writing code
at all. He gives an example with a cache
system, another one with a security hole
in the protocol that hotels use to put
their keys on. Thank you very much. I
have the book with me, if you want to ask
more questions.

(applause)