36C3 - Getting software right with properties, generated tests, and proofs

36C3 preroll music

Herald: Our next talk is held by Mike
Sperber, and he is already very ready for

that. He's head of a software company in
Tübingen in Germany and he's going to talk

about "Getting software right with
properties, generator tests and proofs".

And the main thing here is functional
programming. One tiny thing you might not

know about him is that 1986 he won a
federal competition on IT and so give him

a warm applause for that and also for his
talk.

applause

Mike Sperber: Thank you very much. So is
anybody actively using the induction loop

feature in the first couple of rows? Cuz
I know somebody who would like to know.

Not right now. Okay. Anyway, so let me get
one shameless plug of advertising out of

the way. If you find the contents of this
talk interesting, we're running a

developer conference in Berlin in February
called Bob, which is very friendly and

very nice, very tiny compared to this one.
And we'd love to see you there. Another

thing, this is an introductory talk. So if
you were expecting the latest developments

on proof tactic, in fact, if you know what
proof tactic is, then all you might get

from this talk is sort of mild amusement.
And I won't be mad at you at all if you go

for one of the more exciting talks. Ok?
So. Or leave at any time. That's perfectly

fine, if this material is not for you.
Speaking of introductory talks, here's a

piece of code written in the language that
I will use for this talk and it's called

Idris. Who has written an Idris program
before? Very good. Ok. Oh, there's one

person back there. That means if any part
of this program, as soon as I'm done

explaining, is not clear to you, it's also
not clear to two or three hundred other

people in this room. And I would love to
have your help. Interrupt me, ask a

question anytime in the talk if there's
anything here not clear. It's going to

get, even though it's meant to be
introductory, will get quite technical at

times. So let me try explaining this one.
So this is a classic example in functional

programming that I use often in my talks,
about animals on the Texas Highway. And if

you can see there, the central definition
says data Animal. That's the data

definition of animals. And in this
particular version of the Texas Highway,

there's two different kinds of animals.
There is Armadillo, it's where it says

Dillo there. And there's Parrots, for some
reason, on the Texas Highway. Does that

make sense? Two different kinds of
animals. And you see that definition.

Yeah, nod, that greatly helps me. And if
you see those two definitions for Dillo

and Parrot, you can see, while the arrows
are kind of funny, but you can see that

Dillo and Parrots have two properties
each, and it says their Liveness. That's

one of the properties of an armadillo. And
up there at the very top, you see the

definition of Liveness, it says Liveness
means dead or alive. It's an armadillo,

can be dead or alive on the Texas Highway.
And there's also the Weight. And well, you

see, this colon thing is the type
signature for the constructor for

armadillos. So it says there's a liveness
going on, there's a weight going on, and

then it constructs an animal. And for a
Parrot, there's a string. Every parrot

speaks, right? And so it's the sentence
the Parrot says, and also the Weight. And

it also produces an animal. And, up there,
you can see the definition of Weight is

for simplicity's sake, I'm saying that
Weight is a type. So that's kind of

unusual for Idris, but you don't have to
worry about it. But you can see there,

Weight is just the same thing as an
integer. And if you look down there, where

it says a1, a2 and a3, that has three
examples for animals. So it says a1:

Animal, just to say that a1 is an animal.
So, Idris is a language that always has

type declarations. And it says a1 is Dillo
Alive 10. And that means it's an

armadillo, it's still alive, and it
weighs, let's say, ten kilograms. The

second one is dead, a little bit heavier,
weighs twelve kilograms. And the third

animal is a parrot that knows, well, it's
a pirate's parrot, obviously, and maybe

weighs three kilograms. Ok, so far? Ok. So
if you have any question about any of

that, then please ask away. So, what
happens to animals on the Texas Highway

is, you know, people drive cars, they run
them over. So there's a function down

here, and, well, we're doing functional
programing, shouldn't worry you at all.

But what's important here is that it says
there is an animal going in, an animal

going out. And really what this means is
that this animal object up there is not

really the animal. It is the state of the
animal at a given time. So, runOverAnimal.

you can see the type signature that says
an animal goes in, an animal goes out. And

what it really means is, the state of the
animal goes in before it gets run over and

the state of the animal after it gets run
over comes out. And then while we know

there's two different kinds of animals.
And that means that for the definition of

runOverAnimal, we need what's called
equations. There's two different

equations. And the first equation says
what happens to armadillos when they get

run over. So an armadillo has a liveness
and a weight. Here's something going on

called pattern matching. And the second
equation says when there's a parrot going

on it has a sentence and a weight, and on
the right hand side, you can see, well,

when an armadillo gets run over. Well, all
that means is, the liveness sort of turns

to Dead. We're constructing a new
armadillo object and it's dead and it has

the same weight as before. And the
function, the equation at the bottom says,

well, when we run over a parrot, it turns
really, really quiet. Ok? So, classic

example. Ok so far. We're going to return
to that example at the very end. Right now

it's just to illustrate the language that
we're doing things in and we're going to

do a lot of things without complicated
programs. So, well. So, I'm going to jump

around a little bit. So, one thing. So,
just the other day, two weeks ago, I was

teaching a course on architecture and
somebody said: Well, there's this problem.

I'm building a domain model. I'm putting
the domain model in a database. And, you

know, customer comes in, has new
requirement or somebody comes in, has new

requirements. And that always ends the
same way. I put a new call in the database

and, you know, seven, eight, nine, it just
goes on and on. As the software gets older

and older and older, more columns that
create the old ones seem a little stale.

And so, yes, well, how can we build models
that are flexible? And so, here's

something completely different, you might
think. So, here's sort of the key to that,

to building flexible models. Does anybody
recognize this? Does anybody associate a

word with this? laughter Very good. So,
you might remember, depending on what

state you went to school in, you might
remember that this is a property called

associativity. Right? And it means that we
can associate either the A and the B first

with the parentheses or the B and the C.
So, and this is, if you take away one

thing from this talk, it's associativity.
Knowing what that is is one of the most

useful things in software development. So,
of course it's just a generic equation, we

really need to be more specific, namely
that we're dealing with numbers and

addition. And you might know that it's not
just addition that's associative. Also,

multiplication, for example, is
associative. So here's a little mathy

stuff there at the beginning. So, you see
that upside down A. That says "for all".

We just say for all. What that means is
"for all A, B and C". And then, this funny

epsilon-shape letter kind of thing, it
means "element of". And then that funky N

means the natural numbers. So all the
numbers from zero, one, two, three, the

whole numbers from zero on up. So, what
that means is, for all natural numbers A,

B and C, the associative property holds
when you add them up. But while it says

numbers in addition, it doesn't just hold
for numbers and, addition, in fact,

associativity is everywhere around us.
Specifically, it's everywhere around us

when we program. So here's another
example. When you're dealing with lists

and that funky, the two pluses that you
see there, they are just list

concatenation. So you concatenate two
lists and well, of course you can

concatenate three lists by just using that
double plus in any order. And that's also

associative. So, it doesn't matter if you
first concatenate the B and the C and then

tack the A onto the front, or if you
concatenate the A and B and tack the C on

at the end. Doesn't matter, you always get
the same result. So lists and

concatenation also have this associative
property. And here's something that I

always find very, very enlightening is
that you can construct images that way.

Well, you don't see it here. So here's an
image. Well, it's from a cool researcher

of mine and functional programing, Brent
Yorgey, and he has a great library out

called diagrams, for constructing diagrams
out of parts. And so this really is what

associativity is about. It's about
operators that construct things out of

parts. And so, as you can see here, well
there's different shapes here, there's

sort of the black rectangles, there's a
different rectangle set, that denote the

towers of Hanoi. We're not really going to
deal with the towers of Hanoi here,

really. The important thing that the image
consists of several parts. And well, in

normal or sort of in classic object-
oriented programming, when you do

graphics, you have a canvas and you might
draw pixels on that canvas. You know,

might be square shaped or a circle shaped
canvas pixels. But what we're doing here

is, we are treating an image as a data
type and the definition is not important.

What is important is that there are a
couple of functions that construct sort of

simple images. So here's a function that
you might imagine called star and it

constructs stars. And well, you can see up
there there's a type declaration and it

says, well, the star function, it accepts
an integer, it accepts a Mode, whatever

that is, accepts a Color and it produces
an Image. And we can call that star

function with the arguments 200 and Solid
and Gold. So Mode is Solid or Outline. And

then we have a Color and we get Image and
that image is an object. Not particularly

exciting. But while we might have another
function called Polygon, Polygon takes two

integers that denote the size of the
polygon and the number of vertices, and

also whether it's an outline or whether
it's solid and a color. And for example,

if we call it with 180, again, that's the
size and 5 we get a five corner polygon

and we get that as an outline and it's in
red. Now, the idea here is that we can

combine. Just as we can combine two
numbers or we can combine two lists, we

can combine two images. Maybe the most
intuitive way of combining two images is

just sticking them beside each other. So
there's a function there called beside.

And it takes an image and it takes another
image and produces an image. Right. And

this is exactly what we're thinking about
when we talk about associativity. We're

talking about a sort of a binary operator
that produces the same thing that went in.

And so, for example, we could stick those
two images next to each other. We could

also imagine an operator called above that
just puts one image above the other image.

And we can combine these two things. Here
it really is important that the same thing

comes out so that it's image goes in,
another image goes in, an image goes out.

So we could again call above on the result
of beside and make arrangements. So here's

a tiling arrangement for your bathroom or
something like that. Now, beside and above

are are two possible operators and you
might already think about associativity,

but really the more fundamental one is
overlay. You put two images on top of each

other. And so again, overlay has the right
type. An image goes in, another image goes

in, and an image comes out. And if we take
the gold star and the pentagon and put

them on top of each other, then it looks
like this. And we can then formulate an

associativity property. It might not quite
look the same because I wrote overlay in

front rather than between the operators.
We could also write it between. But just

to show you that it's the same idea. So,
it doesn't really matter if we first take

two images, A and B and superimpose those
two and then put those two on top of C or

if we do it in another order. Does that
make sense so far? Ok. No? Do you have a

question?
Anonymous: Mumbling

Mike: Yeah, so ahh, good point, good
point. So this implies that there must be

some kind of, that there's probably some
notion of transparency involved. Yes. Yes,

there is. But then you have associativity.
And really what it means. Very good

question. So, if you think of this image
in terms of the color at certain

coordinates, Right, Well, you need to
think about how to combine those two

colors that are in the constituent images.
And you can imagine that there also has to

be a combination operation for the colour.
And that also needs to be associative as a

prerequisite for the for the overlay
operation to be associative. Does that

make sense now? Thank you. Good question.
Great question. So anyway, so since this

associativity property is something that
is not just restricted to numbers, as we

may have learned in school, it really
makes sense to get. And that means that

when we talk about associativity, we
always have to name two things. We have to

say what set we're operating on and what
the operation is. And the combination

those two things has a name in mathematics
and it's not the best name, but it's

called a semigroup. Right. And, but, you
know, if you drop it in certain circles,

they'll think that you're an expert on
mathematics, you might try that. So, just

to go over that: So, you have some subset
S, and that S might be Image, it might be

the natural numbers or something like
that. And we have an operation that I'm

just gonna call circle here, then take any
a, b and c from that set S. We can use

circle as an operator and we have that
associativity property and for that circle

you can put in overlay, you can put in
beside, you can put in above, you can put

in + you can put in times or you can put
in the list concatenation operator, the

++. Okay? And that associativity is great.
It's really my favorite property because

it means when we have a whole lot of
things that we combine, we can

parenthesise in any way we want. We will
get the same result no matter which way we

parenthesise them. And that really means,
we can leave out the parentheses when we

write an expression that involves only the
circle operator if it's associative, if we

can just leave out all the parentheses
because the parentheses don't matter. And

that makes it well, that makes it
instantly easier to read, I think. Also it

has practical uses. So if you do big data
processing associativity means that if you

have large datasets that span several
machines or several hard drives or several

data sources, and you're combining them
and you have an associative combination

operation, it just means you can rearrange
that combination operation according to

the load in your compute cluster. And that
makes it a very useful property when

you're doing big data processing in sort
of MapReduce based frameworks. But, I

mean, that's a practical application, but
I think it's much more useful,

associativity is much more useful when you
use it for designing your domain model.

And I talked in the beginning how, well,
you want to avoid always adding more

database columns. And one way of doing
that is to view your domain model, not as

something that has more and more
properties, but your domain model as

building blocks that you combine into a
larger building blocks the same way that

we combine images from simpler images. So
here's one of the great papers from

functional programing, one of my two or
three favorites from Brent Yorgey. And

it's called "Something Something: Theme
and Variations". And you can see that it

is about images. And these images get
superimposed with an operation that is

just like overlay and that is, that title
is eminently googleable. Now, it has a

funny word there. It says, it doesn't say
semigroup, could say"Semigroup: Theme and

Variation", it says "Monoid: Theme and
Variation". And a monoid, well, it's also

not something, even though it sounds kind
of fancy, it's actually not much more

complicated than a semigroup. It's a
semigroup. And also the semigroup has a

special element called the neutral
element. And whenever we combine something

with a neutral element, it doesn't matter
if we do it in front or at the back, we

get the same thing back. So, of course,
the neutral element with respect to

numbers, in addition, would be zero. The
neutral element with respect to lists and

and concatenation would be the empty list.
I always hear several voices. That's

wonderful. Thank you. And the same thing
for the overlay and beside and above, you

can imagine that you have just an empty
image that has only, that consists only of

transparency, that can work as the neutral
element. So all of these things that I

showed you that are associative, they're
not just associative. They're not just

semigroups, they're also monoids. And so,
as I said, as long as you remember

associativity, that's the important thing.
But often you also find a monoid, and

monoids in the wild they're just
everywhere. We've seen them for numbers

and lists and images, music forms a
natural monoid. You can you can describe

musical structure with monoid operations.
You can treat animations, the time axis.

You can define monoidal combination of
animations. A famous example in functional

programming is with financial contracts.
If you were here last year for a talk of

mine, we talked about semiconductor-
fabrication routes, which sounds very

concrete, but also they form a monoid. The
properties themselves that we'll see for a

monoid are all kinds of things. They're
everywhere around you. And these are

really the key towards making flexible
domain models because in almost any domain

model you can find a monoid just by
looking for building blocks and for ways

of combining those building blocks into a
larger building blocks. So let me get

back. So I said, well, you can use
associativity or you can use this monoid

thing to guide your design. And I haven't
really made that concrete yet. And so I

stole a couple of pictures from Brent's
paper. So you remember the beside and the

above operations. And those are fine for
arranging things sort of in the vertical

and the horizontal axis. The way that they
work is, they make, they put a bounding

box around every picture and then they
arrange the bounding boxes either beside

each other or above each other. So it's a
slightly more involved thought. And that

works great when you're, when, you know,
your picture is, happens to be a square

that's aligned with the axes. It doesn't
work so well if your picture is rotated,

right. Because the bounding box, the
bounding box then is too big. And if you

want to attach anything about, just about
in any direction, then there's going to be

a gap in your picture. And so beside and
above are not particularly good operations

as the basis for an image library. The
overlay operation is much better. But that

leaves open the question how you can
arrange pictures, several pictures so that

they are beside each other or that they
just touch. And Brent came up with this

idea of an envelope, technical idea. So
the idea is that, well, if you give me, so

the red dot there, that's the origin. If
you give me a vector starting at the

origin, I will tell you how far you have
to go along that vector so that I can draw

that blue perpendicular line that's just
outside the shape. And that's called an

envelope. And envelopes are wonderful. So
if you ship each picture not just with

sort of the visuals that you see, but also
with a function that describes the

envelope, then you can use that envelope
to arrange pictures both in the horizontal

and the vertical, but also in the diagonal
by just drawing vectors so that they

touch. So, that's a slightly more
complicated idea. Does it make sense? And

Brent goes through the motions of using
that inspiration from the monoid that he

is getting. He's saying "Everything must
be a monoid! Absolutely.", and uses that

as a guiding principle through the
library. So I'm not going to go into

technical detail on how that works, but
it's a very pleasing paper to read on

that. And it results in a beautiful
library that's great fun to use. So that

means, though, that you also have to find
a monoidal combination operation for the

envelopes. You can't just, we've already
seen how we can combine the pictures

themselves, but we also need to combine
the envelopes. And fortunately, that's

pretty easy. If somebody sets a vector in
a certain direction, then that envelope is

just a maximum. Those two pictures, right,
if you combine that ellipse and that

square, you can see that I'm just going to
have to go to the maximum of those two

numbers in order to just be outside the
composite shape that that comes up

superimposing those two things. So that's
great. Now, I sort of introduced these

properties as a mathematical thing, right.
I said, well, there's this fancy, fancy

upside down operator says for all images
and we might say for all images. Now, we

can also formulate these properties as
code. And that's really where additional

magic is. So, for example, the
associativity property, well, there's not

much of a difference except that the
image1 and image2, they are now in

typewriter font. So we could put those in
the program. But there's still that

mathematical stuff on top. But in a
functional language, in a lot of other

languages too by now, we could also put
the top line and translate that into code.

And it might look like this. So that's
what it looks like in Idris. So, it's not

quite the same, but maybe we recognize the
structure. So, we say, well, there's a

property called and the property is just
called overlayAssociative. So we give it a

name. So, Idris is an ASCII language,
still so, primarily. So, we say just

forAll there instead of the upside down
all. And then it says arbTriple arbImage

arbImage arbImage. And that means for all
arbitrary triples of arbitrary images and

other arbitrary image and another
arbitrary image, so, triples, three

things. And we're going to call those
three images image1, image2 and image3.

That funky backslash there, that's a
Lambda in Idris. And then the overlay prop

means that while, if we overlay one way
and we overlay another way, according to

associativity, we get the same result. Do
you recognize that structure? Right. That

it's the same thing. So that we're writing
structurally the same thing that we wrote

in mathematical notation. Now as a piece
of code. And now the great thing is once

we've written it as a piece of code, we
can manipulate it in a program.

So, one way, there is different ways
of manipulating it. But one of the most

useful ones is, again by another great
researcher in functional programming,

John Hughes, came up with something called
QuickCheck. So if there's another thing

you take away from this talk is: google
QuickCheck. And whatever language you use,

it doesn't have to be Idris. In fact, I
had to hack together a QuickCheck for this

talk, but basically any other language is
going to have a QuickCheck, whether that

language be a functional language or
whether it's Java or Python or R or

something like that. You can always get a
QuickCheck for that. And I'm going to try

and demonstrate this QuickCheck thing not
by thinking about the design so much, but

by demonstrating a property of something
that's very error prone. So, here's this

idea, we want to have a representation for
sets of natural numbers. And we're going

to represent those sets of natural numbers
by a list of intervals. So, by a list of

ranges, if you will, between two numbers.
Now, I'll try to explain that. So, up

there at the top, it has a type
definition. It says, ISet, interval set,

is a type. And that type is defined to be
just a synonym for a list of pairs of

natural numbers. That's what those round
parentheses with a comma in the middle

mean. OK. And just to see what that means
is, there's a function there. I haven't,

I've lighted the definition, but what's
important about it is its type signature.

It takes an interval set and it produces a
list of all of the members of that set.

And you can see sort of a demo thing here
that I typed in before the talk. So, if I

apply iToList so that, the brackets there
they just mean the list, and we feed in a

list of intervals and those intervals are
from zero to three, from five to seven,

and from nine to ten, respectively.
They're all inclusive. And you can see

down there is a list of all of the
members. So, the first interval is from 0

to 3. So, it has the numbers 0, 1, 2 and
3. The next one goes from five to seven.

So it has the three numbers 5, 6, 7. And
the last one goes from nine to ten. So it

has the two numbers, 9 and 10 there. Does
that make any sense again? Slightly more

complicated example. So let's see. So, of
course, well, not of course, but the way

we want to do it, the way I want to do it
is, I want to have the interval set

structured in a certain way. I don't just
want any list of any pair of numbers to

denote an interval set. And therefore,
here is a function that describes what it

needs to be a valid interval set. Right.
So, for example, we don't really, in order

to have efficient processing, we don't
really want two intervals in one interval

set to overlap. Right. We want them to be
disjoint and we also want them to be

ordered so we can have efficient
operations for certain things. Right. And

so, let's go through this. So, there is an
isValid function that just tells you

whether that interval set is valid or not.
It says, well, if that set, and there's

three different cases here, which is why
there's three different equations, in the

first equation says the empty interval
set, the empty brackets mean the empty

list, and if the intervals, the list
representing the interval set is empty,

then we're going to say True. Empty set -
perfectly fine. The next case says, our

interval set consists only of a single
interval and that single interval goes

from low to high. Well, we kind of
interpret that there, but, and, well, that

interval set is valid, if low comes in
front of high. Right, they shouldn't be

the other way around. So, does that make
sense? Somebody in, can you nod at the

back, a little bit? You're still there?
OK. Thank you. Great. So, then it becomes

a little bit more complicated and it says,
well, this is the third case, when there's

at least two intervals in the interval
set. And those two intervals are, the

first one goes from lo1 to hi1. The second
one goes from lo2 to hi2. So, those ::,

they separate the first element of a list
from the rest. And then there's the rest

of the list. And it says, well, again, we
want the interval to be ordered so that

the lower numbers are on the left. That's
where it says lo1 is less or equal hi1.

And then it says, well, that there should
be a gap between two consecutive

intervals. Otherwise, they should be one
interval, which is why the high from one

interval should be separated from the low
of the next interval by at least one. And

then we're going to say, well, also we
want all the rest of the list, including

lo2 and hi2 to be valid too. So far so
good? OK, so this is probably, well, the

second most complicated piece of code. So,
anyway, so, here's, so, we might imagine a

union function. And the union function,
guess what, it forms a monoid, with

respect to interval sets. So, it takes,
two internal sets go in and another one

comes out. And if you've written that kind
of thing before, you might notice it's

probably a little tricky with that fancy
validity condition that's there. So how

can we get this right? Well, what we do is
we write down properties. Of course, we

could write down associativity. I'll leave
that as an exercise. Another one is just

very simple. Just a very simple property
that says for all pairs of two arbitrary

interval sets, we want the union of those
two interval sets to be valid, a valid

data structure. We want the union function
to preserve validity. OK? Makes sense? So

here's another property that says, well, I
already gave you this function or I told

you that there is this function iToList,
which just gives us a list of elements of

an interval set. And what we can do is, we
can use sort of that representation,

that's also a representation for sets. We
can use that representation sort of as a

model and say, well, if we take the
unions, you see there for all pairs,

again, of arbitrary interval sets, we take
the union. It says iUnion, iset1 and

iset2. And we convert that to a list. And,
we could also do, we could instead convert

each individual set to a list and then
just merge those two lists. And that

should yield the same result. So, in a
way, we're just giving a very simple model

for our interval sets, right, and that
would, so those two criteria would be kind

of nice to have in order to get our
implementation correct. And I already got

started before the talk on this. Looks
like this. No. Doesn't look like this.

We'll get to that later. But like this.
So, here's what I came up with. So, you

see there is that, while there's all this
other code there, ignore that. But there

is iUnion says ISet -> ISet -> ISet, do
you see that? And then, there's two

equations that say, well, the first set is
empty, then I'm just going to give you the

second one. And if the second one is
empty, I'm just going to give you the

first one. Right? Classic things when you
have union or concatenation operations or

something like that. And now you can see
the third case. It gets tricky, right?

Again, you don't need, I mean, main thing
is you need to understand it's tricky.

Well, the third one is such that, well,
says so that both have at least one

element and that element is in the
interval lo1 and hi1 in the first case and

lo2 and hi2 in the second case. And then
there's the rest. And I already put in a

little bit of code, and I said, well if
lo1 comes after hi1 (means hi2), then we

want to start with lo2 to hi2 and then
continue with the union. In the other

case, if lo2 comes after hi2 (means hi1),
then we're gonna start with lo1 and hi1.

And in the other case, it means, that no
interval comes before the other, and

therefore we need to merge the two
intervals at the beginning. Does that make

remote sense? Right. Don't worry. We'll
get back on solid track. So, we just take

the minimum of those two intervals and
maximum of those two intervals and we do

this. Now, the great thing is, I told you
about this tool by John Hughes called

QuickCheck. And the great thing is, we can
load this into Idris. And then here comes

a REPL, and we can say, I hope I'm doing
this right. So, we want QuickCheck, and we

want, what was it called? It was called
prop_unionCorrect. I hope I'm doing this

right. And, well, very small font. But you
can see here it says "100 tests". And that

is what QuickCheck does, as, it takes your
code version off the property and

automatically generates a lot of tests for
them. And that is super effective at

weeding out bugs. So it says, well, the
thing that you wrote is correct. It always

produces interval sets that when you take
the list, it gives you the right result.

But there was that other criterion called
unionValid. And there it says, and this is

really the better part, of course, of
QuickCheck is, when it fails, it says it's

falsifiable. It says there is a counter
example. And so, here it says, I did nine

tests, I generated nine random tests, and
I found one where the result is not valid.

And the great thing is that we can then go
and cut and paste this example. So I could

say iUnion, this, remove the comma in the
middle, and call this. And well, what

happens here is, what we can see is, we
can see 2 and 4, 1 and 1, and 3 and 5, and

what's not valid about. So, by the way,
this is randomized. So, this always goes

differently. So I have to look at it, too.
So, then it says, well, those two

intervals, they should really just be
merged and they should just be one

interval. Right? And so, it didn't do that
correctly. And the reason for that, maybe

you saw it. So, and, what happened is that
it ran into one of those two cases here

where it says if lo1 greater than hi2 or
lo2 greater than hi1. Remember that I told

you there needs to be a gap of at least
one between them. Remember? And here's an

off-by-one error that says, well. So this
says, they can, lo1 greater than hi2 says

they can still be right next to each
other. Right? And this is what happened

here. We need to make sure that there is
that gap in here. So, I can fix it like

this. Loaded again. Oh, no. There's still
a counterexample. So, and we can try that

out, so, and that's great. We get test
cases that sort of show where the bugs

are. And in this case, well, what happened
here? They still overlap. And what

happened here? So can you see it? So, you
can see that the first two intervals, they

must run into that last case. Right.
Because they overlap. Zero is the interval

from 0 to 3 and the interval from 0 to 5.
They overlap. So we need to get to that

case. And so it merges them. And then it
went and and somehow didn't merge it with

the 6 and the 7 that's there. And, so,
well, if you look at it. So it must have

done this. And and what it did is, it then
went on with the rest there. Let's have

one more look. What actually happened? So
there it is. So, it merged those and then

you can see that it went into a symmetry
problem here. Well, maybe you don't see.

But, you know, this is tricky stuff. I
couldn't do this by myself. So you can see

here that it just tacks the result onto
iset1Rest, whereas the maximum of hi1 and

hi2 could, might violate the consistency
criteria if it's the wrong one, and then

it runs into one of the other cases. Now
I've never seen this tricky one. Does it

make sense? But, can you see that it
should be symmetrical? The last one. Can

you see it? OK, so we'll try and make it
symmetrical. Do it like this. So we'll

say, well, if so, this only works. So if
hi1 is less than hi2. So we really need to

make sure, then it is perfectly. And then
the maximum of those two numbers is hi1.

Does that make sense? And so the max of
those two numbers is hi1 and then it's

perfectly valid to tack it onto iset1Rest.
In the other case, hi2 is greater and we

need to go and do something different and
rip this out here. Stick it in front here

and then. And then. And now it's
symmetrical. OK. So, load this. And, ahh!

It has passed the test. OK, live great.
applause

Thank you. I did practice getting it
correct, right. But you can, you know,

this kind of stuff. It always gets me. I
mean, you know, with old age especially,

this kind of stuff, it always drives the
sweat on my forehead, right? You know,

there's off-by-one. There is, you know, I
don't know how many cases there need to

be. And QuickCheck is the kind of thing
that weeds out the bugs. And even though

it weeds out the bugs in a different order
each time, it always weeds them all out.

OK. So it's a great tool. Now, I recommend
that you try that. It generates tests from

properties. OK, where are we? So let me
let me give you a couple of real world

examples. So if you're using X windows,
there's a there's a tiling, a window

manager, xmonad. It's already a couple of
years old and they don't do much

development on it anymore. That's because
it's correct. Right. laughter Right. And

why is it correct? Well, it's because they
wrote down a lot of properties for the

geometry and the tiling algorithms and
verified them using QuickCheck. And so I

sort of loosely translated. So, Don
Stewart, one of the authors of xmonad

graciously wrote a couple of blog posts on
a simplified version of xmonad and I

translated them into Idris. So, here's a
very simple idea of just a stacking window

manager. So, it doesn't do geometry, it
just has stacks of windows and it has

several workspaces. In each workspace is a
stack of windows. So here's a data type

called a StackSet, its parameterized by a
type called window. We'll see later why

there's a type parameter and why it just
doesn't say what the windows are. And then

it says there's a constructor StackSet
and there's two fields in there. One is

called "current", that's the number of the
workspace that's currently

active. And then there's "stacks",
which is a map from the number of the

workspace to the stack of, to the list of
windows that sit in that workspace. Again,

so here, really the technicalities are
not particularly important, but there is a

bunch of operations that operate on this
window manager configuration. And again,

here, really the details aren't important.
So you could create an empty stack set.

You could say, well, you know, I have the
number of a window that I want to get to

the front. And please make me, please
rotate me, the stack set around so that I

can see it. "peek" means, you know, maybe
I can get the topmost window that the user

is currently looking at. "rotate" means
I'm just going to rotate the workspaces

around in either left or right direction.
That's what that ordering argument. "push"

is, I push a new window onto the current
workspace. "insert" means insert a window

into one of the other workspaces. "delete"
means I delete a window. "shift" means,

also means I shift something with the
windows. Not really important what they

do. But you can imagine again, just as we
did with the interval sets is validity

criterion or an invariant that should hold
for these operations. And it's very

simple. Well, it says well, if you have a
stack set with some windows in it, I'm

just going to tell you whether that stack
set is consistent. And by doing that, I'm

just going to say, well, the current, the
number of the current stack

should not be higher than the number of
window stacks that there are. Right. So,

the number of stacks that there are. And
the other one, that just says a window

should not be in several of the
workspaces. Right? And then I can go and

maybe with this definition, all
those function definitions aren't very

complicated. But, I can go and write a
whole bunch of properties. And if you just

understand, well, maybe the second one,
"prop_view_I", you understand all of them.

It just says, well, for all pairs of a
natural number and a stack set that are a

"stackIndex" and "stackSet", I want, if I
call the "view" function, which is one of

the operations, I want the view function
to produce a consistent stack set. And

then it goes on to do all of that for all
the other ones. At the bottom here, you

can see some prerequisites that need to
hold for the property so that invariant

only needs to hold if the window, if the
number of the window is actually smaller

than the size of the stack set. Otherwise,
I think the function just returns what

would go with it, what went in there, So
that's a very, that's just a very

efficient way to invent properties, to
think of some invariant that shall hold in

your data structure. And if you know
Idris, you can sometimes encode that in

the types, but often that's kind of
tedious. And you can just write it down as

a property and then have QuickCheck check
it for you. And it's not particularly

exciting for the simple definition, but
you can imagine that the actual definition

when you have tiling window management
going on is much more complicated than the

one that you just saw. But you can keep
those same properties, right? There still

needs to be some consistency invariant
that, if you have tilings, the windows

don't overlap, and things like that. That
should be obvious. Write those properties

down, check them using QuickCheck and that
will weed out a lot of the bugs.

Here's an example from our
practice. We, couple months ago, we were

tasked with migrating a giant Visual Basic
6 application. It had a password checking

function there. You can see here a Visual
Basic 6 type signature. And the property

that we wrote was, well, if we create the
hash from the password and we compare it

with the hash that's in the database, then
they should all come out the same. And to

our surprise, that function, that test,
that property, failed when we ran it for

QuickCheck and we had to correct it
because that password hash is restricted

to 11 characters by some restriction in
the database schema. And so that means

that you can use QuickCheck not just to
sort of check the correctness of things

that you already know, but to actually
develop a model for what goes on in your

software, which you don't always know very
well. So that's what we did there. Another

example is, we wrote, for a large
industrial client, we needed to write a

synchronization application. So when you
had two mobile devices and they would sort

of meet as strangers, they would exchange
data and they all needed to look at the

same sort of device configuration data.
And we didn't want them to exchange all

the data every single time. We just wanted
to exchange them, the data blocks that the

other side was missing. And again, there's
great algorithms for this based on Merkle

trees. They're pretty complicated. You
have to do a lot of bit fiddling with

that. But fortunately, the property for
that is pretty easy to write. So here's

the property that says, well, so the
synchronization algorithm works on sets of

blocks, whatever a block is. So you can
see the property here for all pairs of

sets of blocks and more sets of blocks. So
they're called bs1 and bs2. Block set one

and block set two. What we can do is, we
want, if we union those two, then we get

all the blocks in the system. We call that
all, or we can call the synchronization

algorithm and that will give us two new
block sets, block set bs1' and bs2'. And

those block sets are the ones that get
transferred to the other side. OK. And the

criterion here just says if we take the
ones that we have, if we union them with

the ones that we get, we should get all of
them. That should be all of them. And that

should be the same for both sides. And
also, we want the algorithm to be

efficient so we don't want it to transfer
blocks. So we want to make sure that the

blocks that we have and the blocks that we
get are disjoint. That they don't have any

elements in common. Otherwise, we could
make that algorithm trivially correct by

just transferring all the blocks every
single time. And I can tell you, I

sweated. You know, I sweated one or two
weeks over this algorithm and it was

really hard to write. But this one test
weeded out all the bugs that I found along

the way. So that is just super, super
effective. John Hughes has a couple of

papers on hard bugs that he found. So he
found a bug in a distributed database

called mnesia. And that bug was dependent
on opening the database, closing it and

opening it again. So this is not the kind
of bug that you find by just writing a

bunch of smart unit tests. Right? So, if
you did anything shorter in the beginning,

so if you just open the file and then did
some lookups there, that would not

manifest the bug. You really needed to
close and then open again. Have you

turned, have you tried turning it off and
on again? But then the database breaks in

this case. And here's another example
called The Mysteries of Dropbox. So you

can imagine that with Dropbox you really
want certain properties to hold. Right?

And it turns out they didn't. They never
worried about writing properties down. But

John Hughes did it and found a couple of
bugs. So here's one. It's kind of hard to

read where it says client 1 writes a into
a file that was previously empty. So that

funky turnstile there is empty. So writes
a into a file and then deletes the file

and another client writes, replaces, sees
the a in the file replaces it with a b.

And then client 1 goes and writes c into
the file that it previously thought to be

empty. And then unfortunately, even though
you can imagine that you should see either

b or c in that file, but Dropbox deleted
it. So I think they fixed that bug now.

But. so you go. So it goes. Oscar Wikstrom
has a couple of great, pretty recent blog

posts on properties in a screencasts
editor that I highly recommend. So this is

a great tool for finding bugs, but it's
not the same as having a proof. Right? So,

you can still imagine that you can find
very subtle bugs that are not covered by

QuickCheck. QuickCheck just randomizes,
just generates randomized tests. So, that

is not the same thing as making sure that
there aren't any bugs. So the great thing

about Idris and the reason I chose it for
this talk is that Idris allows you to not

just encode properties in the language. It
also allows you to encode proofs in the

language. So here is the associative
property for the list concatenation

operation. And if you look at the top that
has the definition of that function from

the Idris standard library, it says ++, in
goes a list, in goes another list, out

comes a list. Then it says, well, if you
concatenate the empty list with any list,

that is just that list "right". Do you
see that? The second one says, well, if we

concatenate a list that starts with the
element x and goes on with xs, then we

just sort of pull the x in front and
concatenate the rest with "right". So

that's a classic recursive definition of
list concatenation in functional

programming. And now here's something
really strange in Idris. Here's the type

declaration for a definition, again in the
standard library, called appendAssoc. And

it says, if you have a list a, you have a
list b, and you have a list c, and in the

type it says, oh, the associative property
should hold. Right. And so this is a

statement of that property. That's
wonderful. It's not the same as a proof.

So, but writing proofs, who loved that in
math? Oh. Oh, you're good! I didn't. I'm

sorry. So. So the great thing about Idris
is, it helps you write down the proofs.

I'll show you how that works just really,
really briefly. So here's that. So here's

just what I showed you on that slide. So I
can load that in there and it says, well,

you're not done. You didn't write a proof
for that property, but in Idris, you can

just push a bunch of buttons. Now, I love
that. So I can push one button and it

says, oh, well, you should write a proof
of that form. You have lists a, b and c.

Well, now and I can push another button
that says, well, you're doing this on

lists and if you're writing anything on
lists, you always need to distinguish

between the two cases of the empty list
and the list that consists of the first

element x and further element xs. And then
it says, well, write down something, but

then I can tell Idris: Well, I'm too lazy.
I'm not going to write anything so I can

just push a button. And Idris wrote this
so you can see me, but I didn't type this

right. I just pushed a button and it says,
Refl. What is Refl? What could that be?

Well, you can ask it what Refl is. It says
Refl. Oh, you can see here, landing here.

Refl is just a proof sort of a built in
proof that says that if two things are

true, two things are equal, if they're
identical, if they're the same. Right. And

that kind of makes sense in the first
equation, because the first equation of

appendAssoc corresponds to the first
equation of ++. Can you see that, how it

corresponds? Can you see that? The first
list is empty. Can you see that? Can you

see how the first list is empty with the
first equation of appendAssoc and the

first list is empty up there with ++. Can
you see that? OK. And then it just says,

well, then obviously. Well, not quite
obviously, but then sort of the the way

that the definition works, it comes out
just right. So what's really important is

that Idris accepts that proof with the
first. The second one is slightly more

tricky. But again, we can get help because
we know that appendAssoc is this recursive

function. It recurses on the first
argument. So we're just going to do the

same thing in the proof. And you can tell
Idris that it should use that, that it

should use that fact, if you will. So
here's the recursive call. And again, I'm

too lazy to push a button. But if I push
that button, it also puts in Refl and

there's loads. So this it might be a
mystery to you how it works, but this is a

proof of the associate of property of the
list concatenation in Idris. And since

Idris helps you write it, it's kind of fun
to do that. Oddly enough, even for

somebody who doesn't, usually who doesn't
usually doesn't enjoy proofs. So the way

that you program in Idris, we haven't done
that a lot in this talk, is that you put a

lot of information in the types and the
more information you put in the types, the

better Idris will get at figuring out the
correct definition. And you don't have to

do it by yourself. OK. So that's really
nice. OK. So we got that and and sort of

these kinds of proof assisting systems
such as Idris have been used in a lot of

real world systems. One one prominent
example is SEL4, a version of the L4

micro kernel, has a long history, but
important properties of that kernel have

been verified. It runs in the security
enclave on iOS and even though it's

written in C, it provably does not have
buffer overflows or a lot of the nasty

things that are responsible for a lot of
security exploits. Compcert is another

example, which is a verified, I should
mention this has been verified with the

help of a tool called Isabel. Also, great
fun to use. There's a project called

called Compcert, which is a verified C
compiler, which is important for a lot of

certified software where, you know, the
source code might be certified. But how do

you know that the compiler generates
correct code? And you know, because it's

been proven to be correct. And even there,
you can shoot, you can cheat sometimes. So

for example, register allocators, very
complicated, very hard to prove right.

But what you can do is you can write a
checker that the register allocator did

its job, did its job well and you can
verify the checker. And so you can cheat a

bit. So there's tools for that. We've seen
Idris and there's a number of other tools

and they're getting more and more mature.
And they're great fun, really. They really

are great fun. But, you know, going back,
switching down a gear a little bit,

there's lots of useful properties that you
can look for in your programs. So

commutativity might be useful that you can
switch the two arguments for an operation.

Also, if you have relations, you might
remember that from some math class,

there's some properties here like
reflexivity, symmetry, antisymmetry and

transitivity. Reflexivity says that a is
always related to a. Symmetry says if it's

one way, if a and b are one way related,
they need to be related the other way too.

Antisymmetry intuitively would seem kind
of the opposite. That doesn't make sense.

It's just says: if two things are related
in both both ways around. So, for example,

you know, orders like less or equal are
antisymmetrical, then they must be the

same. And transitivity just says that you
can form chains of your relation. So those

are a little dictionary of useful
properties that you can look for. Let me

close with one fancy property that you've
probably seen somewhere and that property

is called Functor. And you might have seen
in your programing language, in your list

library or in your stream library. There's
a function called map, right? And you

know, even Java has that and has had it
for many years. And what map does is, if

you have some, you know, in Java, for
example, it says "Stream", or it might be

"List", right. It says, well, if I have a
list of As, I can apply a function to each

element of that list. But you can
generalize that, it doesn't have to be

lists. It could be an Optional of As, for
example. You could also apply a function

to the value that's in there. So, you can
generalize that notion, and then it's a

functor. And, of course, in Idris, you can
write down equations for functors. And,

please ignore the technicalities here,
(stammers) but, if you sort of pick out

where it says "functorIdentity",
the middle row says g v equals to v,

which means g is the identity
function. When you feed in v, you always

get v back. And when you use map with the
identity function, you apply the identity

function on each element of your list or
whatever it is. Then then you always get

back the same list. And here just says you
get function composition. So if you apply

one function and then another function and
you do that either inside or outside the

map, you should also get the same results.
So there's also just as there is

associativity with monoids, with functors.
There's these laws and you might think,

well, where would I look for a functor?
I've never seen a functor except for the

ones on streams. A couple weeks ago in a
training, somebody said, well, you always

start with that animal example. Shouldn't
you look for a functor there? And I was

kind of, you know, sweat broke out on my
forehead, I was like, where's that gonna

go? But, we came up with this. So, if you
go back, you can see that this is obvious.

So, what you need for functors is, you
need a type parameter. Right. And so you

just look for a place to stick a type
parameter, any place here at all. And

if you look at Dillo and Parrot, they
both prominently have this weight thing.

Right. And so that seems more important
than the other two properties, which are

specific to particular kind of animal. And
so the weight, the thing to do is just to,

well, you can see I replaced upper case
Weight by lower case weight and made that

into a type parameter, and, I can then
provide a functor implementation down

there. And you might think, what is that
good for? Well, I don't know. Well, one

thing that you could do is you could
provide a different representation for

weights. Another thing that you could do,
if you look at the type for runOverAnimal,

it says animal weight -> animal weight and
weight is a type variable. What that type

signature tells you is that runOverAnimal
does not know what weight is. And that

means that the weight cannot change as a
result of that function. And you see that

in the type signature you get immediate,
small benefit, but you get a benefit even

with silly examples such as this one. And
that really brings me to the end. So in

your software, in your domain model, look
for a Combinator, look for a function that

will combine two things into a bigger
thing. See if you can make that thing

associative and look for a neutral
element. And very often you will find one;

make it a monoid, you know, say monoid a
couple of times. You'll remember it.

You'll remember it. Generally, write
properties for the things, for the

operations in your software, test those
properties using QuickCheck. You know, if

you feel like you have a lot of time,
prove them correct. Find the functor. If

you found, if you found the monoid, you
know, find the functor next. You know, and

it takes, it might take time. I'm
very old. As you noticed at the beginning.

So. So it gets easier over the years and
it will just seem like a regular staple of

your of your arsenal when you program. And
of course, when the important properties

in your program have either been written
down, if they've been tested with

QuickCheck or even proven, then you can
sleep much more soundly than maybe you

currently can. Thank you very much.
applause

Herald: Thank you, Mike. So I see we have
three minutes for questions. Maybe that's

two or three questions. If you have any
come to the microphones, please. Do we

have a question from the Internet? No, not
yet. So, microphone two. Right.

Question: Hi. So, QuickCheck generated
hundred tests. Yes. What can we say about

the quality of this test? Could we say
your program was correct using thoese

tests? Are these tests good?
Answer: Yeah. Very good question. So what

would you say about the quality of the
tests? And indeed, if you really do serve

industrial strength applications, a quick
QuickCheck comes with a bunch of tools

that let you look, for example, at the
distribution of the individual example

rated and while you didn't quite see me do
that, but I mean, for your domain objects,

you will typically write generators that
will generate those examples and you can

reason about the distribution of those.
And you absolutely should do that because

otherwise you might miss large areas of
your test space. So, but there

are tools and they help you do that. But
even if you don't do that, you know, it's,

you find a lot of, I found a lot of
bugs in my software even without worrying

about that. But if you go beyond that,
look at the distribution thing.

Herald: Thank you, next one, please.
Number two.

Q: Let's say I've hacked a program, for
example, in Java or C# or whatever. How do

I, how do I apply what I learned so
far? So, where do I start when I have

already completed the C# program with,
yeah, how do I apply QuickCheck on that?

A: So, just pragmatically because it's
written in C#? That's the question?

Q: Yes
A: So, well, I have to be very concrete

here, I mean, so, if you can think
properties, right, one way to do, so,

for example, so, C# you can link with F#
and there is a QuickCheck version for F#

called "FsCheck". And FsCheck, actually,
even though it's itself written in F#, you

can also use it from C#. So, you have two
options. You can write your tests in a

slightly more awkward fashion in C#, or
you could just link your code with F# test

suite and write it down there. And there
is a fairly reasonable Java QuickCheck, I

hear. Another idea would be to use the
slightly more fancier, the slightly

fancier QuickChecks that exist for Scala
and Enclosure. I'm sure there's one for

Kotlin as well, and link that against your
Java code. Does that answer your question?

Q: So whatever language I use, I have to
find out what the correct implementation

of QuickCkeck?
A: Yeah. Yeah. But as I said, I mean

usually, a fun thing I do in training is,
I chat "QuickCheck" and somebody calls on

the language, you know. Quick, QuickCheck
PHP or something like that. And there is

one, sure enough, I didn't know about before.
Q: Thank you.

Herald: All right. Thank you. And thank
you, Mike, again, for showing us a way to

sleeping soundly.
A: Thank you.

applause

postroll music

Subtitles created by c3subtitles.de
in the year 2020. Join, and help us!