0:00:00.000,0:00:19.369
<i>36C3 preroll music</i>

0:00:19.369,0:00:25.550
Herald: Our next talk is held by Mike[br]Sperber, and he is already very ready for

0:00:25.550,0:00:31.009
that. He's head of a software company in[br]Tübingen in Germany and he's going to talk

0:00:31.009,0:00:36.540
about "Getting software right with[br]properties, generator tests and proofs".

0:00:36.540,0:00:42.470
And the main thing here is functional[br]programming. One tiny thing you might not

0:00:42.470,0:00:50.740
know about him is that 1986 he won a[br]federal competition on IT and so give him

0:00:50.740,0:00:53.870
a warm applause for that and also for his[br]talk.

0:00:53.870,0:00:58.220
<i>applause</i>

0:00:58.220,0:01:04.690
Mike Sperber: Thank you very much. So is[br]anybody actively using the induction loop

0:01:04.690,0:01:09.110
feature in the first couple of rows? Cuz[br]I know somebody who would like to know.

0:01:09.110,0:01:17.080
Not right now. Okay. Anyway, so let me get[br]one shameless plug of advertising out of

0:01:17.080,0:01:22.230
the way. If you find the contents of this[br]talk interesting, we're running a

0:01:22.230,0:01:26.170
developer conference in Berlin in February[br]called Bob, which is very friendly and

0:01:26.170,0:01:32.580
very nice, very tiny compared to this one.[br]And we'd love to see you there. Another

0:01:32.580,0:01:39.570
thing, this is an introductory talk. So if[br]you were expecting the latest developments

0:01:39.570,0:01:44.280
on proof tactic, in fact, if you know what[br]proof tactic is, then all you might get

0:01:44.280,0:01:48.890
from this talk is sort of mild amusement.[br]And I won't be mad at you at all if you go

0:01:48.890,0:01:56.160
for one of the more exciting talks. Ok?[br]So. Or leave at any time. That's perfectly

0:01:56.160,0:02:01.791
fine, if this material is not for you.[br]Speaking of introductory talks, here's a

0:02:01.791,0:02:05.740
piece of code written in the language that[br]I will use for this talk and it's called

0:02:05.740,0:02:12.160
Idris. Who has written an Idris program[br]before? Very good. Ok. Oh, there's one

0:02:12.160,0:02:17.810
person back there. That means if any part[br]of this program, as soon as I'm done

0:02:17.810,0:02:22.129
explaining, is not clear to you, it's also[br]not clear to two or three hundred other

0:02:22.129,0:02:26.540
people in this room. And I would love to[br]have your help. Interrupt me, ask a

0:02:26.540,0:02:30.250
question anytime in the talk if there's[br]anything here not clear. It's going to

0:02:30.250,0:02:34.799
get, even though it's meant to be[br]introductory, will get quite technical at

0:02:34.799,0:02:41.120
times. So let me try explaining this one.[br]So this is a classic example in functional

0:02:41.120,0:02:46.139
programming that I use often in my talks,[br]about animals on the Texas Highway. And if

0:02:46.139,0:02:49.680
you can see there, the central definition[br]says data Animal. That's the data

0:02:49.680,0:02:54.189
definition of animals. And in this[br]particular version of the Texas Highway,

0:02:54.189,0:02:58.189
there's two different kinds of animals.[br]There is Armadillo, it's where it says

0:02:58.189,0:03:03.860
Dillo there. And there's Parrots, for some[br]reason, on the Texas Highway. Does that

0:03:03.860,0:03:07.389
make sense? Two different kinds of[br]animals. And you see that definition.

0:03:07.389,0:03:14.430
Yeah, nod, that greatly helps me. And if[br]you see those two definitions for Dillo

0:03:14.430,0:03:18.529
and Parrot, you can see, while the arrows[br]are kind of funny, but you can see that

0:03:18.529,0:03:23.930
Dillo and Parrots have two properties[br]each, and it says their Liveness. That's

0:03:23.930,0:03:27.689
one of the properties of an armadillo. And[br]up there at the very top, you see the

0:03:27.689,0:03:31.519
definition of Liveness, it says Liveness[br]means dead or alive. It's an armadillo,

0:03:31.519,0:03:36.919
can be dead or alive on the Texas Highway.[br]And there's also the Weight. And well, you

0:03:36.919,0:03:41.710
see, this colon thing is the type[br]signature for the constructor for

0:03:41.710,0:03:45.979
armadillos. So it says there's a liveness[br]going on, there's a weight going on, and

0:03:45.979,0:03:49.989
then it constructs an animal. And for a[br]Parrot, there's a string. Every parrot

0:03:49.989,0:03:54.150
speaks, right? And so it's the sentence[br]the Parrot says, and also the Weight. And

0:03:54.150,0:03:58.590
it also produces an animal. And, up there,[br]you can see the definition of Weight is

0:03:58.590,0:04:02.442
for simplicity's sake, I'm saying that[br]Weight is a type. So that's kind of

0:04:02.442,0:04:06.150
unusual for Idris, but you don't have to[br]worry about it. But you can see there,

0:04:06.150,0:04:10.830
Weight is just the same thing as an[br]integer. And if you look down there, where

0:04:10.830,0:04:16.549
it says a1, a2 and a3, that has three[br]examples for animals. So it says a1:

0:04:16.549,0:04:21.480
Animal, just to say that a1 is an animal.[br]So, Idris is a language that always has

0:04:21.480,0:04:26.610
type declarations. And it says a1 is Dillo[br]Alive 10. And that means it's an

0:04:26.610,0:04:31.210
armadillo, it's still alive, and it[br]weighs, let's say, ten kilograms. The

0:04:31.210,0:04:35.500
second one is dead, a little bit heavier,[br]weighs twelve kilograms. And the third

0:04:35.500,0:04:40.590
animal is a parrot that knows, well, it's[br]a pirate's parrot, obviously, and maybe

0:04:40.590,0:04:48.062
weighs three kilograms. Ok, so far? Ok. So[br]if you have any question about any of

0:04:48.062,0:04:52.260
that, then please ask away. So, what[br]happens to animals on the Texas Highway

0:04:52.260,0:04:56.540
is, you know, people drive cars, they run[br]them over. So there's a function down

0:04:56.540,0:05:01.100
here, and, well, we're doing functional[br]programing, shouldn't worry you at all.

0:05:01.100,0:05:04.870
But what's important here is that it says[br]there is an animal going in, an animal

0:05:04.870,0:05:09.520
going out. And really what this means is[br]that this animal object up there is not

0:05:09.520,0:05:15.820
really the animal. It is the state of the[br]animal at a given time. So, runOverAnimal.

0:05:15.820,0:05:19.770
you can see the type signature that says[br]an animal goes in, an animal goes out. And

0:05:19.770,0:05:24.400
what it really means is, the state of the[br]animal goes in before it gets run over and

0:05:24.400,0:05:29.920
the state of the animal after it gets run[br]over comes out. And then while we know

0:05:29.920,0:05:34.260
there's two different kinds of animals.[br]And that means that for the definition of

0:05:34.260,0:05:37.910
runOverAnimal, we need what's called[br]equations. There's two different

0:05:37.910,0:05:41.640
equations. And the first equation says[br]what happens to armadillos when they get

0:05:41.640,0:05:45.840
run over. So an armadillo has a liveness[br]and a weight. Here's something going on

0:05:45.840,0:05:50.700
called pattern matching. And the second[br]equation says when there's a parrot going

0:05:50.700,0:05:54.690
on it has a sentence and a weight, and on[br]the right hand side, you can see, well,

0:05:54.690,0:05:59.360
when an armadillo gets run over. Well, all[br]that means is, the liveness sort of turns

0:05:59.360,0:06:03.320
to Dead. We're constructing a new[br]armadillo object and it's dead and it has

0:06:03.320,0:06:09.210
the same weight as before. And the[br]function, the equation at the bottom says,

0:06:09.210,0:06:15.180
well, when we run over a parrot, it turns[br]really, really quiet. Ok? So, classic

0:06:15.180,0:06:20.940
example. Ok so far. We're going to return[br]to that example at the very end. Right now

0:06:20.940,0:06:24.820
it's just to illustrate the language that[br]we're doing things in and we're going to

0:06:24.820,0:06:32.210
do a lot of things without complicated[br]programs. So, well. So, I'm going to jump

0:06:32.210,0:06:36.020
around a little bit. So, one thing. So,[br]just the other day, two weeks ago, I was

0:06:36.020,0:06:40.120
teaching a course on architecture and[br]somebody said: Well, there's this problem.

0:06:40.120,0:06:43.958
I'm building a domain model. I'm putting[br]the domain model in a database. And, you

0:06:43.958,0:06:47.430
know, customer comes in, has new[br]requirement or somebody comes in, has new

0:06:47.430,0:06:51.260
requirements. And that always ends the[br]same way. I put a new call in the database

0:06:51.260,0:06:55.810
and, you know, seven, eight, nine, it just[br]goes on and on. As the software gets older

0:06:55.810,0:07:01.330
and older and older, more columns that[br]create the old ones seem a little stale.

0:07:01.330,0:07:08.250
And so, yes, well, how can we build models[br]that are flexible? And so, here's

0:07:08.250,0:07:12.950
something completely different, you might[br]think. So, here's sort of the key to that,

0:07:12.950,0:07:16.800
to building flexible models. Does anybody[br]recognize this? Does anybody associate a

0:07:16.800,0:07:23.020
word with this? <i>laughter</i> Very good. So,[br]you might remember, depending on what

0:07:23.020,0:07:26.810
state you went to school in, you might[br]remember that this is a property called

0:07:26.810,0:07:31.910
associativity. Right? And it means that we[br]can associate either the A and the B first

0:07:31.910,0:07:38.200
with the parentheses or the B and the C.[br]So, and this is, if you take away one

0:07:38.200,0:07:42.860
thing from this talk, it's associativity.[br]Knowing what that is is one of the most

0:07:42.860,0:07:47.060
useful things in software development. So,[br]of course it's just a generic equation, we

0:07:47.060,0:07:51.025
really need to be more specific, namely[br]that we're dealing with numbers and

0:07:51.025,0:07:54.880
addition. And you might know that it's not[br]just addition that's associative. Also,

0:07:54.880,0:07:58.670
multiplication, for example, is[br]associative. So here's a little mathy

0:07:58.670,0:08:03.760
stuff there at the beginning. So, you see[br]that upside down A. That says "for all".

0:08:03.760,0:08:09.030
We just say for all. What that means is[br]"for all A, B and C". And then, this funny

0:08:09.030,0:08:13.850
epsilon-shape letter kind of thing, it[br]means "element of". And then that funky N

0:08:13.850,0:08:17.490
means the natural numbers. So all the[br]numbers from zero, one, two, three, the

0:08:17.490,0:08:22.790
whole numbers from zero on up. So, what[br]that means is, for all natural numbers A,

0:08:22.790,0:08:29.720
B and C, the associative property holds[br]when you add them up. But while it says

0:08:29.720,0:08:33.500
numbers in addition, it doesn't just hold[br]for numbers and, addition, in fact,

0:08:33.500,0:08:37.819
associativity is everywhere around us.[br]Specifically, it's everywhere around us

0:08:37.819,0:08:41.680
when we program. So here's another[br]example. When you're dealing with lists

0:08:41.680,0:08:45.100
and that funky, the two pluses that you[br]see there, they are just list

0:08:45.100,0:08:50.449
concatenation. So you concatenate two[br]lists and well, of course you can

0:08:50.449,0:08:55.809
concatenate three lists by just using that[br]double plus in any order. And that's also

0:08:55.809,0:09:00.730
associative. So, it doesn't matter if you[br]first concatenate the B and the C and then

0:09:00.730,0:09:06.029
tack the A onto the front, or if you[br]concatenate the A and B and tack the C on

0:09:06.029,0:09:09.750
at the end. Doesn't matter, you always get[br]the same result. So lists and

0:09:09.750,0:09:17.249
concatenation also have this associative[br]property. And here's something that I

0:09:17.249,0:09:22.139
always find very, very enlightening is[br]that you can construct images that way.

0:09:22.139,0:09:27.470
Well, you don't see it here. So here's an[br]image. Well, it's from a cool researcher

0:09:27.470,0:09:31.610
of mine and functional programing, Brent[br]Yorgey, and he has a great library out

0:09:31.610,0:09:37.019
called diagrams, for constructing diagrams[br]out of parts. And so this really is what

0:09:37.019,0:09:40.839
associativity is about. It's about[br]operators that construct things out of

0:09:40.839,0:09:44.740
parts. And so, as you can see here, well[br]there's different shapes here, there's

0:09:44.740,0:09:48.500
sort of the black rectangles, there's a[br]different rectangle set, that denote the

0:09:48.500,0:09:52.180
towers of Hanoi. We're not really going to[br]deal with the towers of Hanoi here,

0:09:52.180,0:09:57.989
really. The important thing that the image[br]consists of several parts. And well, in

0:09:57.989,0:10:01.300
normal or sort of in classic object-[br]oriented programming, when you do

0:10:01.300,0:10:05.639
graphics, you have a canvas and you might[br]draw pixels on that canvas. You know,

0:10:05.639,0:10:11.170
might be square shaped or a circle shaped[br]canvas pixels. But what we're doing here

0:10:11.170,0:10:18.079
is, we are treating an image as a data[br]type and the definition is not important.

0:10:18.079,0:10:23.350
What is important is that there are a[br]couple of functions that construct sort of

0:10:23.350,0:10:28.671
simple images. So here's a function that[br]you might imagine called star and it

0:10:28.671,0:10:33.790
constructs stars. And well, you can see up[br]there there's a type declaration and it

0:10:33.790,0:10:37.949
says, well, the star function, it accepts[br]an integer, it accepts a Mode, whatever

0:10:37.949,0:10:42.209
that is, accepts a Color and it produces[br]an Image. And we can call that star

0:10:42.209,0:10:48.750
function with the arguments 200 and Solid[br]and Gold. So Mode is Solid or Outline. And

0:10:48.750,0:10:53.980
then we have a Color and we get Image and[br]that image is an object. Not particularly

0:10:53.980,0:11:00.140
exciting. But while we might have another[br]function called Polygon, Polygon takes two

0:11:00.140,0:11:05.759
integers that denote the size of the[br]polygon and the number of vertices, and

0:11:05.759,0:11:09.759
also whether it's an outline or whether[br]it's solid and a color. And for example,

0:11:09.759,0:11:17.079
if we call it with 180, again, that's the[br]size and 5 we get a five corner polygon

0:11:17.079,0:11:23.390
and we get that as an outline and it's in[br]red. Now, the idea here is that we can

0:11:23.390,0:11:27.490
combine. Just as we can combine two[br]numbers or we can combine two lists, we

0:11:27.490,0:11:31.629
can combine two images. Maybe the most[br]intuitive way of combining two images is

0:11:31.629,0:11:36.560
just sticking them beside each other. So[br]there's a function there called beside.

0:11:36.560,0:11:41.009
And it takes an image and it takes another[br]image and produces an image. Right. And

0:11:41.009,0:11:44.820
this is exactly what we're thinking about[br]when we talk about associativity. We're

0:11:44.820,0:11:50.709
talking about a sort of a binary operator[br]that produces the same thing that went in.

0:11:50.709,0:11:55.640
And so, for example, we could stick those[br]two images next to each other. We could

0:11:55.640,0:12:01.249
also imagine an operator called above that[br]just puts one image above the other image.

0:12:01.249,0:12:05.270
And we can combine these two things. Here[br]it really is important that the same thing

0:12:05.270,0:12:09.519
comes out so that it's image goes in,[br]another image goes in, an image goes out.

0:12:09.519,0:12:14.529
So we could again call above on the result[br]of beside and make arrangements. So here's

0:12:14.529,0:12:18.829
a tiling arrangement for your bathroom or[br]something like that. Now, beside and above

0:12:18.829,0:12:23.930
are are two possible operators and you[br]might already think about associativity,

0:12:23.930,0:12:28.990
but really the more fundamental one is[br]overlay. You put two images on top of each

0:12:28.990,0:12:33.279
other. And so again, overlay has the right[br]type. An image goes in, another image goes

0:12:33.279,0:12:38.199
in, and an image comes out. And if we take[br]the gold star and the pentagon and put

0:12:38.199,0:12:46.089
them on top of each other, then it looks[br]like this. And we can then formulate an

0:12:46.089,0:12:51.559
associativity property. It might not quite[br]look the same because I wrote overlay in

0:12:51.559,0:12:56.314
front rather than between the operators.[br]We could also write it between. But just

0:12:56.314,0:13:00.250
to show you that it's the same idea. So,[br]it doesn't really matter if we first take

0:13:00.250,0:13:05.209
two images, A and B and superimpose those[br]two and then put those two on top of C or

0:13:05.209,0:13:13.319
if we do it in another order. Does that[br]make sense so far? Ok. No? Do you have a

0:13:13.319,0:13:16.390
question?[br]Anonymous: <i>Mumbling</i>

0:13:16.390,0:13:20.970
Mike: Yeah, so ahh, good point, good[br]point. So this implies that there must be

0:13:20.970,0:13:24.910
some kind of, that there's probably some[br]notion of transparency involved. Yes. Yes,

0:13:24.910,0:13:29.480
there is. But then you have associativity.[br]And really what it means. Very good

0:13:29.480,0:13:38.399
question. So, if you think of this image[br]in terms of the color at certain

0:13:38.399,0:13:43.600
coordinates, Right, Well, you need to[br]think about how to combine those two

0:13:43.600,0:13:48.670
colors that are in the constituent images.[br]And you can imagine that there also has to

0:13:48.670,0:13:53.329
be a combination operation for the colour.[br]And that also needs to be associative as a

0:13:53.329,0:13:58.600
prerequisite for the for the overlay[br]operation to be associative. Does that

0:13:58.600,0:14:07.669
make sense now? Thank you. Good question.[br]Great question. So anyway, so since this

0:14:07.669,0:14:11.589
associativity property is something that[br]is not just restricted to numbers, as we

0:14:11.589,0:14:15.229
may have learned in school, it really[br]makes sense to get. And that means that

0:14:15.229,0:14:18.979
when we talk about associativity, we[br]always have to name two things. We have to

0:14:18.979,0:14:22.679
say what set we're operating on and what[br]the operation is. And the combination

0:14:22.679,0:14:28.369
those two things has a name in mathematics[br]and it's not the best name, but it's

0:14:28.369,0:14:34.040
called a semigroup. Right. And, but, you[br]know, if you drop it in certain circles,

0:14:34.040,0:14:39.100
they'll think that you're an expert on[br]mathematics, you might try that. So, just

0:14:39.100,0:14:43.029
to go over that: So, you have some subset[br]S, and that S might be Image, it might be

0:14:43.029,0:14:46.640
the natural numbers or something like[br]that. And we have an operation that I'm

0:14:46.640,0:14:53.570
just gonna call circle here, then take any[br]a, b and c from that set S. We can use

0:14:53.570,0:14:57.769
circle as an operator and we have that[br]associativity property and for that circle

0:14:57.769,0:15:02.389
you can put in overlay, you can put in[br]beside, you can put in above, you can put

0:15:02.389,0:15:08.899
in + you can put in times or you can put[br]in the list concatenation operator, the

0:15:08.899,0:15:15.759
++. Okay? And that associativity is great.[br]It's really my favorite property because

0:15:15.759,0:15:20.119
it means when we have a whole lot of[br]things that we combine, we can

0:15:20.119,0:15:24.560
parenthesise in any way we want. We will[br]get the same result no matter which way we

0:15:24.560,0:15:28.839
parenthesise them. And that really means,[br]we can leave out the parentheses when we

0:15:28.839,0:15:33.070
write an expression that involves only the[br]circle operator if it's associative, if we

0:15:33.070,0:15:36.839
can just leave out all the parentheses[br]because the parentheses don't matter. And

0:15:36.839,0:15:41.889
that makes it well, that makes it[br]instantly easier to read, I think. Also it

0:15:41.889,0:15:46.870
has practical uses. So if you do big data[br]processing associativity means that if you

0:15:46.870,0:15:52.040
have large datasets that span several[br]machines or several hard drives or several

0:15:52.040,0:15:58.679
data sources, and you're combining them[br]and you have an associative combination

0:15:58.679,0:16:03.259
operation, it just means you can rearrange[br]that combination operation according to

0:16:03.259,0:16:07.579
the load in your compute cluster. And that[br]makes it a very useful property when

0:16:07.579,0:16:12.220
you're doing big data processing in sort[br]of MapReduce based frameworks. But, I

0:16:12.220,0:16:16.410
mean, that's a practical application, but[br]I think it's much more useful,

0:16:16.410,0:16:21.220
associativity is much more useful when you[br]use it for designing your domain model.

0:16:21.220,0:16:25.749
And I talked in the beginning how, well,[br]you want to avoid always adding more

0:16:25.749,0:16:29.559
database columns. And one way of doing[br]that is to view your domain model, not as

0:16:29.559,0:16:33.220
something that has more and more[br]properties, but your domain model as

0:16:33.220,0:16:37.439
building blocks that you combine into a[br]larger building blocks the same way that

0:16:37.439,0:16:42.749
we combine images from simpler images. So[br]here's one of the great papers from

0:16:42.749,0:16:46.439
functional programing, one of my two or[br]three favorites from Brent Yorgey. And

0:16:46.439,0:16:50.219
it's called "Something Something: Theme[br]and Variations". And you can see that it

0:16:50.219,0:16:54.940
is about images. And these images get[br]superimposed with an operation that is

0:16:54.940,0:17:00.589
just like overlay and that is, that title[br]is eminently googleable. Now, it has a

0:17:00.589,0:17:04.540
funny word there. It says, it doesn't say[br]semigroup, could say"Semigroup: Theme and

0:17:04.540,0:17:08.640
Variation", it says "Monoid: Theme and[br]Variation". And a monoid, well, it's also

0:17:08.640,0:17:12.360
not something, even though it sounds kind[br]of fancy, it's actually not much more

0:17:12.360,0:17:16.400
complicated than a semigroup. It's a[br]semigroup. And also the semigroup has a

0:17:16.400,0:17:20.186
special element called the neutral[br]element. And whenever we combine something

0:17:20.186,0:17:24.070
with a neutral element, it doesn't matter[br]if we do it in front or at the back, we

0:17:24.070,0:17:27.790
get the same thing back. So, of course,[br]the neutral element with respect to

0:17:27.790,0:17:33.660
numbers, in addition, would be zero. The[br]neutral element with respect to lists and

0:17:33.660,0:17:38.540
and concatenation would be the empty list.[br]I always hear several voices. That's

0:17:38.540,0:17:42.505
wonderful. Thank you. And the same thing[br]for the overlay and beside and above, you

0:17:42.505,0:17:46.400
can imagine that you have just an empty[br]image that has only, that consists only of

0:17:46.400,0:17:51.530
transparency, that can work as the neutral[br]element. So all of these things that I

0:17:51.530,0:17:55.310
showed you that are associative, they're[br]not just associative. They're not just

0:17:55.310,0:18:00.740
semigroups, they're also monoids. And so,[br]as I said, as long as you remember

0:18:00.740,0:18:04.510
associativity, that's the important thing.[br]But often you also find a monoid, and

0:18:04.510,0:18:07.910
monoids in the wild they're just[br]everywhere. We've seen them for numbers

0:18:07.910,0:18:12.501
and lists and images, music forms a[br]natural monoid. You can you can describe

0:18:12.501,0:18:19.660
musical structure with monoid operations.[br]You can treat animations, the time axis.

0:18:19.660,0:18:24.670
You can define monoidal combination of[br]animations. A famous example in functional

0:18:24.670,0:18:28.630
programming is with financial contracts.[br]If you were here last year for a talk of

0:18:28.630,0:18:32.270
mine, we talked about semiconductor-[br]fabrication routes, which sounds very

0:18:32.270,0:18:37.121
concrete, but also they form a monoid. The[br]properties themselves that we'll see for a

0:18:37.121,0:18:40.690
monoid are all kinds of things. They're[br]everywhere around you. And these are

0:18:40.690,0:18:44.820
really the key towards making flexible[br]domain models because in almost any domain

0:18:44.820,0:18:48.880
model you can find a monoid just by[br]looking for building blocks and for ways

0:18:48.880,0:18:54.330
of combining those building blocks into a[br]larger building blocks. So let me get

0:18:54.330,0:19:00.100
back. So I said, well, you can use[br]associativity or you can use this monoid

0:19:00.100,0:19:04.260
thing to guide your design. And I haven't[br]really made that concrete yet. And so I

0:19:04.260,0:19:09.370
stole a couple of pictures from Brent's[br]paper. So you remember the beside and the

0:19:09.370,0:19:14.380
above operations. And those are fine for[br]arranging things sort of in the vertical

0:19:14.380,0:19:19.900
and the horizontal axis. The way that they[br]work is, they make, they put a bounding

0:19:19.900,0:19:23.930
box around every picture and then they[br]arrange the bounding boxes either beside

0:19:23.930,0:19:28.291
each other or above each other. So it's a[br]slightly more involved thought. And that

0:19:28.291,0:19:32.200
works great when you're, when, you know,[br]your picture is, happens to be a square

0:19:32.200,0:19:36.670
that's aligned with the axes. It doesn't[br]work so well if your picture is rotated,

0:19:36.670,0:19:40.300
right. Because the bounding box, the[br]bounding box then is too big. And if you

0:19:40.300,0:19:44.260
want to attach anything about, just about[br]in any direction, then there's going to be

0:19:44.260,0:19:49.860
a gap in your picture. And so beside and[br]above are not particularly good operations

0:19:49.860,0:19:54.790
as the basis for an image library. The[br]overlay operation is much better. But that

0:19:54.790,0:19:59.100
leaves open the question how you can[br]arrange pictures, several pictures so that

0:19:59.100,0:20:04.940
they are beside each other or that they[br]just touch. And Brent came up with this

0:20:04.940,0:20:12.010
idea of an envelope, technical idea. So[br]the idea is that, well, if you give me, so

0:20:12.010,0:20:17.520
the red dot there, that's the origin. If[br]you give me a vector starting at the

0:20:17.520,0:20:22.580
origin, I will tell you how far you have[br]to go along that vector so that I can draw

0:20:22.580,0:20:27.470
that blue perpendicular line that's just[br]outside the shape. And that's called an

0:20:27.470,0:20:33.960
envelope. And envelopes are wonderful. So[br]if you ship each picture not just with

0:20:33.960,0:20:38.400
sort of the visuals that you see, but also[br]with a function that describes the

0:20:38.400,0:20:43.680
envelope, then you can use that envelope[br]to arrange pictures both in the horizontal

0:20:43.680,0:20:48.470
and the vertical, but also in the diagonal[br]by just drawing vectors so that they

0:20:48.470,0:20:52.580
touch. So, that's a slightly more[br]complicated idea. Does it make sense? And

0:20:52.580,0:20:57.160
Brent goes through the motions of using[br]that inspiration from the monoid that he

0:20:57.160,0:21:02.810
is getting. He's saying "Everything must[br]be a monoid! Absolutely.", and uses that

0:21:02.810,0:21:06.170
as a guiding principle through the[br]library. So I'm not going to go into

0:21:06.170,0:21:11.380
technical detail on how that works, but[br]it's a very pleasing paper to read on

0:21:11.380,0:21:17.560
that. And it results in a beautiful[br]library that's great fun to use. So that

0:21:17.560,0:21:22.050
means, though, that you also have to find[br]a monoidal combination operation for the

0:21:22.050,0:21:25.670
envelopes. You can't just, we've already[br]seen how we can combine the pictures

0:21:25.670,0:21:29.351
themselves, but we also need to combine[br]the envelopes. And fortunately, that's

0:21:29.351,0:21:33.300
pretty easy. If somebody sets a vector in[br]a certain direction, then that envelope is

0:21:33.300,0:21:37.040
just a maximum. Those two pictures, right,[br]if you combine that ellipse and that

0:21:37.040,0:21:41.260
square, you can see that I'm just going to[br]have to go to the maximum of those two

0:21:41.260,0:21:46.700
numbers in order to just be outside the[br]composite shape that that comes up

0:21:46.700,0:21:52.930
superimposing those two things. So that's[br]great. Now, I sort of introduced these

0:21:52.930,0:21:56.920
properties as a mathematical thing, right.[br]I said, well, there's this fancy, fancy

0:21:56.920,0:22:02.830
upside down operator says for all images[br]and we might say for all images. Now, we

0:22:02.830,0:22:08.810
can also formulate these properties as[br]code. And that's really where additional

0:22:08.810,0:22:12.240
magic is. So, for example, the[br]associativity property, well, there's not

0:22:12.240,0:22:15.610
much of a difference except that the[br]image1 and image2, they are now in

0:22:15.610,0:22:19.640
typewriter font. So we could put those in[br]the program. But there's still that

0:22:19.640,0:22:24.130
mathematical stuff on top. But in a[br]functional language, in a lot of other

0:22:24.130,0:22:28.340
languages too by now, we could also put[br]the top line and translate that into code.

0:22:28.340,0:22:32.190
And it might look like this. So that's[br]what it looks like in Idris. So, it's not

0:22:32.190,0:22:37.380
quite the same, but maybe we recognize the[br]structure. So, we say, well, there's a

0:22:37.380,0:22:41.370
property called and the property is just[br]called overlayAssociative. So we give it a

0:22:41.370,0:22:48.100
name. So, Idris is an ASCII language,[br]still so, primarily. So, we say just

0:22:48.100,0:22:52.760
forAll there instead of the upside down[br]all. And then it says arbTriple arbImage

0:22:52.760,0:22:58.930
arbImage arbImage. And that means for all[br]arbitrary triples of arbitrary images and

0:22:58.930,0:23:02.180
other arbitrary image and another[br]arbitrary image, so, triples, three

0:23:02.180,0:23:08.430
things. And we're going to call those[br]three images image1, image2 and image3.

0:23:08.430,0:23:15.150
That funky backslash there, that's a[br]Lambda in Idris. And then the overlay prop

0:23:15.150,0:23:21.460
means that while, if we overlay one way[br]and we overlay another way, according to

0:23:21.460,0:23:26.260
associativity, we get the same result. Do[br]you recognize that structure? Right. That

0:23:26.260,0:23:31.060
it's the same thing. So that we're writing[br]structurally the same thing that we wrote

0:23:31.060,0:23:36.790
in mathematical notation. Now as a piece[br]of code. And now the great thing is once

0:23:36.790,0:23:40.801
we've written it as a piece of code, we[br]can manipulate it in a program.

0:23:40.801,0:23:44.570
So, one way, there is different ways[br]of manipulating it. But one of the most

0:23:44.570,0:23:48.140
useful ones is, again by another great[br]researcher in functional programming,

0:23:48.140,0:23:52.000
John Hughes, came up with something called[br]QuickCheck. So if there's another thing

0:23:52.000,0:23:55.870
you take away from this talk is: google[br]QuickCheck. And whatever language you use,

0:23:55.870,0:24:00.530
it doesn't have to be Idris. In fact, I[br]had to hack together a QuickCheck for this

0:24:00.530,0:24:04.400
talk, but basically any other language is[br]going to have a QuickCheck, whether that

0:24:04.400,0:24:08.730
language be a functional language or[br]whether it's Java or Python or R or

0:24:08.730,0:24:15.490
something like that. You can always get a[br]QuickCheck for that. And I'm going to try

0:24:15.490,0:24:22.560
and demonstrate this QuickCheck thing not[br]by thinking about the design so much, but

0:24:22.560,0:24:28.090
by demonstrating a property of something[br]that's very error prone. So, here's this

0:24:28.090,0:24:35.230
idea, we want to have a representation for[br]sets of natural numbers. And we're going

0:24:35.230,0:24:40.800
to represent those sets of natural numbers[br]by a list of intervals. So, by a list of

0:24:40.800,0:24:44.991
ranges, if you will, between two numbers.[br]Now, I'll try to explain that. So, up

0:24:44.991,0:24:49.510
there at the top, it has a type[br]definition. It says, ISet, interval set,

0:24:49.510,0:24:56.650
is a type. And that type is defined to be[br]just a synonym for a list of pairs of

0:24:56.650,0:25:00.380
natural numbers. That's what those round[br]parentheses with a comma in the middle

0:25:00.380,0:25:05.340
mean. OK. And just to see what that means[br]is, there's a function there. I haven't,

0:25:05.340,0:25:10.000
I've lighted the definition, but what's[br]important about it is its type signature.

0:25:10.000,0:25:15.610
It takes an interval set and it produces a[br]list of all of the members of that set.

0:25:15.610,0:25:20.920
And you can see sort of a demo thing here[br]that I typed in before the talk. So, if I

0:25:20.920,0:25:27.260
apply iToList so that, the brackets there[br]they just mean the list, and we feed in a

0:25:27.260,0:25:32.240
list of intervals and those intervals are[br]from zero to three, from five to seven,

0:25:32.240,0:25:36.860
and from nine to ten, respectively.[br]They're all inclusive. And you can see

0:25:36.860,0:25:40.460
down there is a list of all of the[br]members. So, the first interval is from 0

0:25:40.460,0:25:47.040
to 3. So, it has the numbers 0, 1, 2 and[br]3. The next one goes from five to seven.

0:25:47.040,0:25:51.490
So it has the three numbers 5, 6, 7. And[br]the last one goes from nine to ten. So it

0:25:51.490,0:25:56.580
has the two numbers, 9 and 10 there. Does[br]that make any sense again? Slightly more

0:25:56.580,0:26:05.760
complicated example. So let's see. So, of[br]course, well, not of course, but the way

0:26:05.760,0:26:09.521
we want to do it, the way I want to do it[br]is, I want to have the interval set

0:26:09.521,0:26:15.870
structured in a certain way. I don't just[br]want <i>any</i> list of any pair of numbers to

0:26:15.870,0:26:19.660
denote an interval set. And therefore,[br]here is a function that describes what it

0:26:19.660,0:26:25.610
needs to be a valid interval set. Right.[br]So, for example, we don't really, in order

0:26:25.610,0:26:29.430
to have efficient processing, we don't[br]really want two intervals in one interval

0:26:29.430,0:26:33.120
set to overlap. Right. We want them to be[br]disjoint and we also want them to be

0:26:33.120,0:26:37.620
ordered so we can have efficient[br]operations for certain things. Right. And

0:26:37.620,0:26:41.410
so, let's go through this. So, there is an[br]isValid function that just tells you

0:26:41.410,0:26:46.230
whether that interval set is valid or not.[br]It says, well, if that set, and there's

0:26:46.230,0:26:50.140
three different cases here, which is why[br]there's three different equations, in the

0:26:50.140,0:26:54.660
first equation says the empty interval[br]set, the empty brackets mean the empty

0:26:54.660,0:26:58.750
list, and if the intervals, the list[br]representing the interval set is empty,

0:26:58.750,0:27:04.070
then we're going to say True. Empty set -[br]perfectly fine. The next case says, our

0:27:04.070,0:27:08.520
interval set consists only of a single[br]interval and that single interval goes

0:27:08.520,0:27:14.210
from low to high. Well, we kind of[br]interpret that there, but, and, well, that

0:27:14.210,0:27:18.360
interval set is valid, if low comes in[br]front of high. Right, they shouldn't be

0:27:18.360,0:27:23.870
the other way around. So, does that make[br]sense? Somebody in, can you nod at the

0:27:23.870,0:27:29.010
back, a little bit? You're still there?[br]OK. Thank you. Great. So, then it becomes

0:27:29.010,0:27:33.190
a little bit more complicated and it says,[br]well, this is the third case, when there's

0:27:33.190,0:27:38.670
at least two intervals in the interval[br]set. And those two intervals are, the

0:27:38.670,0:27:44.900
first one goes from lo1 to hi1. The second[br]one goes from lo2 to hi2. So, those ::,

0:27:44.900,0:27:48.810
they separate the first element of a list[br]from the rest. And then there's the rest

0:27:48.810,0:27:54.140
of the list. And it says, well, again, we[br]want the interval to be ordered so that

0:27:54.140,0:27:59.380
the lower numbers are on the left. That's[br]where it says lo1 is less or equal hi1.

0:27:59.380,0:28:03.730
And then it says, well, that there should[br]be a gap between two consecutive

0:28:03.730,0:28:09.010
intervals. Otherwise, they should be one[br]interval, which is why the high from one

0:28:09.010,0:28:14.750
interval should be separated from the low[br]of the next interval by at least one. And

0:28:14.750,0:28:18.930
then we're going to say, well, also we[br]want all the rest of the list, including

0:28:18.930,0:28:26.740
lo2 and hi2 to be valid too. So far so[br]good? OK, so this is probably, well, the

0:28:26.740,0:28:32.370
second most complicated piece of code. So,[br]anyway, so, here's, so, we might imagine a

0:28:32.370,0:28:37.341
union function. And the union function,[br]guess what, it forms a monoid, with

0:28:37.341,0:28:43.300
respect to interval sets. So, it takes,[br]two internal sets go in and another one

0:28:43.300,0:28:47.510
comes out. And if you've written that kind[br]of thing before, you might notice it's

0:28:47.510,0:28:52.790
probably a little tricky with that fancy[br]validity condition that's there. So how

0:28:52.790,0:28:58.250
can we get this right? Well, what we do is[br]we write down properties. Of course, we

0:28:58.250,0:29:02.770
could write down associativity. I'll leave[br]that as an exercise. Another one is just

0:29:02.770,0:29:08.740
very simple. Just a very simple property[br]that says for all pairs of two arbitrary

0:29:08.740,0:29:13.890
interval sets, we want the union of those[br]two interval sets to be valid, a valid

0:29:13.890,0:29:21.300
data structure. We want the union function[br]to preserve validity. OK? Makes sense? So

0:29:21.300,0:29:26.580
here's another property that says, well, I[br]already gave you this function or I told

0:29:26.580,0:29:32.710
you that there is this function iToList,[br]which just gives us a list of elements of

0:29:32.710,0:29:36.860
an interval set. And what we can do is, we[br]can use sort of that representation,

0:29:36.860,0:29:40.710
that's also a representation for sets. We[br]can use that representation sort of as a

0:29:40.710,0:29:44.640
model and say, well, if we take the[br]unions, you see there for all pairs,

0:29:44.640,0:29:49.770
again, of arbitrary interval sets, we take[br]the union. It says iUnion, iset1 and

0:29:49.770,0:29:55.570
iset2. And we convert that to a list. And,[br]we could also do, we could instead convert

0:29:55.570,0:30:00.760
each individual set to a list and then[br]just merge those two lists. And that

0:30:00.760,0:30:06.390
should yield the same result. So, in a[br]way, we're just giving a very simple model

0:30:06.390,0:30:10.330
for our interval sets, right, and that[br]would, so those two criteria would be kind

0:30:10.330,0:30:15.940
of nice to have in order to get our[br]implementation correct. And I already got

0:30:15.940,0:30:20.440
started before the talk on this. Looks[br]like this. No. Doesn't look like this.

0:30:20.440,0:30:29.390
We'll get to that later. But like this.[br]So, here's what I came up with. So, you

0:30:29.390,0:30:33.290
see there is that, while there's all this[br]other code there, ignore that. But there

0:30:33.290,0:30:36.961
is iUnion says ISet -&gt; ISet -&gt; ISet, do[br]you see that? And then, there's two

0:30:36.961,0:30:41.120
equations that say, well, the first set is[br]empty, then I'm just going to give you the

0:30:41.120,0:30:44.620
second one. And if the second one is[br]empty, I'm just going to give you the

0:30:44.620,0:30:49.510
first one. Right? Classic things when you[br]have union or concatenation operations or

0:30:49.510,0:30:54.200
something like that. And now you can see[br]the third case. It gets tricky, right?

0:30:54.200,0:30:58.350
Again, you don't need, I mean, main thing[br]is you need to understand it's tricky.

0:30:58.350,0:31:05.840
Well, the third one is such that, well,[br]says so that both have at least one

0:31:05.840,0:31:11.210
element and that element is in the[br]interval lo1 and hi1 in the first case and

0:31:11.210,0:31:15.130
lo2 and hi2 in the second case. And then[br]there's the rest. And I already put in a

0:31:15.130,0:31:20.570
little bit of code, and I said, well if[br]lo1 comes after hi1 (means hi2), then we

0:31:20.570,0:31:25.350
want to start with lo2 to hi2 and then[br]continue with the union. In the other

0:31:25.350,0:31:29.350
case, if lo2 comes after hi2 (means hi1),[br]then we're gonna start with lo1 and hi1.

0:31:29.350,0:31:33.809
And in the other case, it means, that no[br]interval comes before the other, and

0:31:33.809,0:31:38.800
therefore we need to merge the two[br]intervals at the beginning. Does that make

0:31:38.800,0:31:43.980
remote sense? Right. Don't worry. We'll[br]get back on solid track. So, we just take

0:31:43.980,0:31:47.850
the minimum of those two intervals and[br]maximum of those two intervals and we do

0:31:47.850,0:31:52.090
this. Now, the great thing is, I told you[br]about this tool by John Hughes called

0:31:52.090,0:31:58.740
QuickCheck. And the great thing is, we can[br]load this into Idris. And then here comes

0:31:58.740,0:32:10.920
a REPL, and we can say, I hope I'm doing[br]this right. So, we want QuickCheck, and we

0:32:10.920,0:32:16.860
want, what was it called? It was called[br]prop_unionCorrect. I hope I'm doing this

0:32:16.860,0:32:21.840
right. And, well, very small font. But you[br]can see here it says "100 tests". And that

0:32:21.840,0:32:27.100
is what QuickCheck does, as, it takes your[br]code version off the property and

0:32:27.100,0:32:32.130
automatically generates a lot of tests for[br]them. And that is super effective at

0:32:32.130,0:32:36.250
weeding out bugs. So it says, well, the[br]thing that you wrote is correct. It always

0:32:36.250,0:32:43.550
produces interval sets that when you take[br]the list, it gives you the right result.

0:32:43.550,0:32:50.360
But there was that other criterion called[br]unionValid. And there it says, and this is

0:32:50.360,0:32:54.520
really the better part, of course, of[br]QuickCheck is, when it fails, it says it's

0:32:54.520,0:33:00.500
falsifiable. It says there is a counter[br]example. And so, here it says, I did nine

0:33:00.500,0:33:05.070
tests, I generated nine random tests, and[br]I found one where the result is not valid.

0:33:05.070,0:33:11.360
And the great thing is that we can then go[br]and cut and paste this example. So I could

0:33:11.360,0:33:17.810
say iUnion, this, remove the comma in the[br]middle, and call this. And well, what

0:33:17.810,0:33:23.780
happens here is, what we can see is, we[br]can see 2 and 4, 1 and 1, and 3 and 5, and

0:33:23.780,0:33:27.600
what's not valid about. So, by the way,[br]this is randomized. So, this always goes

0:33:27.600,0:33:31.860
differently. So I have to look at it, too.[br]So, then it says, well, those two

0:33:31.860,0:33:35.260
intervals, they should really just be[br]merged and they should just be one

0:33:35.260,0:33:43.711
interval. Right? And so, it didn't do that[br]correctly. And the reason for that, maybe

0:33:43.711,0:33:55.010
you saw it. So, and, what happened is that[br]it ran into one of those two cases here

0:33:55.010,0:33:59.630
where it says if lo1 greater than hi2 or[br]lo2 greater than hi1. Remember that I told

0:33:59.630,0:34:04.630
you there needs to be a gap of at least[br]one between them. Remember? And here's an

0:34:04.630,0:34:11.030
off-by-one error that says, well. So this[br]says, they can, lo1 greater than hi2 says

0:34:11.030,0:34:14.610
they can still be right next to each[br]other. Right? And this is what happened

0:34:14.610,0:34:19.760
here. We need to make sure that there is[br]that gap in here. So, I can fix it like

0:34:19.760,0:34:38.060
this. Loaded again. Oh, no. There's still[br]a counterexample. So, and we can try that

0:34:38.060,0:34:42.940
out, so, and that's great. We get test[br]cases that sort of show where the bugs

0:34:42.940,0:34:51.470
are. And in this case, well, what happened[br]here? They still overlap. And what

0:34:51.470,0:34:59.711
happened here? So can you see it? So, you[br]can see that the first two intervals, they

0:34:59.711,0:35:05.440
must run into that last case. Right.[br]Because they overlap. Zero is the interval

0:35:05.440,0:35:12.920
from 0 to 3 and the interval from 0 to 5.[br]They overlap. So we need to get to that

0:35:12.920,0:35:18.850
case. And so it merges them. And then it[br]went and and somehow didn't merge it with

0:35:18.850,0:35:30.400
the 6 and the 7 that's there. And, so,[br]well, if you look at it. So it must have

0:35:30.400,0:35:38.800
done this. And and what it did is, it then[br]went on with the rest there. Let's have

0:35:38.800,0:35:58.820
one more look. What actually happened? So[br]there it is. So, it merged those and then

0:35:58.820,0:36:02.640
you can see that it went into a symmetry[br]problem here. Well, maybe you don't see.

0:36:02.640,0:36:08.190
But, you know, this is tricky stuff. I[br]couldn't do this by myself. So you can see

0:36:08.190,0:36:18.780
here that it just tacks the result onto[br]iset1Rest, whereas the maximum of hi1 and

0:36:18.780,0:36:25.890
hi2 could, might violate the consistency[br]criteria if it's the wrong one, and then

0:36:25.890,0:36:30.270
it runs into one of the other cases. Now[br]I've never seen this tricky one. Does it

0:36:30.270,0:36:34.110
make sense? But, can you see that it[br]should be symmetrical? The last one. Can

0:36:34.110,0:36:39.960
you see it? OK, so we'll try and make it[br]symmetrical. Do it like this. So we'll

0:36:39.960,0:36:51.640
say, well, if so, this only works. So if[br]hi1 is less than hi2. So we really need to

0:36:51.640,0:36:59.480
make sure, then it is perfectly. And then[br]the maximum of those two numbers is hi1.

0:36:59.480,0:37:05.380
Does that make sense? And so the max of[br]those two numbers is hi1 and then it's

0:37:05.380,0:37:12.100
perfectly valid to tack it onto iset1Rest.[br]In the other case, hi2 is greater and we

0:37:12.100,0:37:18.480
need to go and do something different and[br]rip this out here. Stick it in front here

0:37:18.480,0:37:35.950
and then. And then. And now it's[br]symmetrical. OK. So, load this. And, ahh!

0:37:35.950,0:37:40.619
It has passed the test. OK, live great.[br]<i>applause</i>

0:37:40.619,0:37:47.100
Thank you. I did practice getting it[br]correct, right. But you can, you know,

0:37:47.100,0:37:51.340
this kind of stuff. It always gets me. I[br]mean, you know, with old age especially,

0:37:51.340,0:37:55.530
this kind of stuff, it always drives the[br]sweat on my forehead, right? You know,

0:37:55.530,0:37:59.340
there's off-by-one. There is, you know, I[br]don't know how many cases there need to

0:37:59.340,0:38:03.140
be. And QuickCheck is the kind of thing[br]that weeds out the bugs. And even though

0:38:03.140,0:38:07.060
it weeds out the bugs in a different order[br]each time, it always weeds them all out.

0:38:07.060,0:38:11.770
OK. So it's a great tool. Now, I recommend[br]that you try that. It generates tests from

0:38:11.770,0:38:18.869
properties. OK, where are we? So let me[br]let me give you a couple of real world

0:38:18.869,0:38:23.030
examples. So if you're using X windows,[br]there's a there's a tiling, a window

0:38:23.030,0:38:26.890
manager, xmonad. It's already a couple of[br]years old and they don't do much

0:38:26.890,0:38:33.330
development on it anymore. That's because[br]it's correct. Right. <i>laughter</i> Right. And

0:38:33.330,0:38:39.280
why is it correct? Well, it's because they[br]wrote down a lot of properties for the

0:38:39.280,0:38:45.690
geometry and the tiling algorithms and[br]verified them using QuickCheck. And so I

0:38:45.690,0:38:49.120
sort of loosely translated. So, Don[br]Stewart, one of the authors of xmonad

0:38:49.120,0:38:53.340
graciously wrote a couple of blog posts on[br]a simplified version of xmonad and I

0:38:53.340,0:39:01.580
translated them into Idris. So, here's a[br]very simple idea of just a stacking window

0:39:01.580,0:39:05.280
manager. So, it doesn't do geometry, it[br]just has stacks of windows and it has

0:39:05.280,0:39:10.460
several workspaces. In each workspace is a[br]stack of windows. So here's a data type

0:39:10.460,0:39:17.029
called a StackSet, its parameterized by a[br]type called window. We'll see later why

0:39:17.029,0:39:20.930
there's a type parameter and why it just[br]doesn't say what the windows are. And then

0:39:20.930,0:39:25.140
it says there's a constructor StackSet[br]and there's two fields in there. One is

0:39:25.140,0:39:34.071
called "current", that's the number of the[br]workspace that's currently

0:39:34.071,0:39:37.460
active. And then there's "stacks",[br]which is a map from the number of the

0:39:37.460,0:39:44.070
workspace to the stack of, to the list of[br]windows that sit in that workspace. Again,

0:39:44.070,0:39:48.270
so here, really the technicalities are[br]not particularly important, but there is a

0:39:48.270,0:39:54.090
bunch of operations that operate on this[br]window manager configuration. And again,

0:39:54.090,0:39:58.300
here, really the details aren't important.[br]So you could create an empty stack set.

0:39:58.300,0:40:03.350
You could say, well, you know, I have the[br]number of a window that I want to get to

0:40:03.350,0:40:07.270
the front. And please make me, please[br]rotate me, the stack set around so that I

0:40:07.270,0:40:12.990
can see it. "peek" means, you know, maybe[br]I can get the topmost window that the user

0:40:12.990,0:40:17.070
is currently looking at. "rotate" means[br]I'm just going to rotate the workspaces

0:40:17.070,0:40:21.030
around in either left or right direction.[br]That's what that ordering argument. "push"

0:40:21.030,0:40:25.660
is, I push a new window onto the current[br]workspace. "insert" means insert a window

0:40:25.660,0:40:31.630
into one of the other workspaces. "delete"[br]means I delete a window. "shift" means,

0:40:31.630,0:40:35.720
also means I shift something with the[br]windows. Not really important what they

0:40:35.720,0:40:42.520
do. But you can imagine again, just as we[br]did with the interval sets is validity

0:40:42.520,0:40:46.820
criterion or an invariant that should hold[br]for these operations. And it's very

0:40:46.820,0:40:51.390
simple. Well, it says well, if you have a[br]stack set with some windows in it, I'm

0:40:51.390,0:40:55.320
just going to tell you whether that stack[br]set is consistent. And by doing that, I'm

0:40:55.320,0:41:01.800
just going to say, well, the current, the[br]number of the current stack

0:41:01.800,0:41:07.280
should not be higher than the number of[br]window stacks that there are. Right. So,

0:41:07.280,0:41:11.051
the number of stacks that there are. And[br]the other one, that just says a window

0:41:11.051,0:41:18.280
should not be in several of the[br]workspaces. Right? And then I can go and

0:41:18.280,0:41:22.910
maybe with this definition, all[br]those function definitions aren't very

0:41:22.910,0:41:26.950
complicated. But, I can go and write a[br]whole bunch of properties. And if you just

0:41:26.950,0:41:30.800
understand, well, maybe the second one,[br]"prop_view_I", you understand all of them.

0:41:30.800,0:41:35.770
It just says, well, for all pairs of a[br]natural number and a stack set that are a

0:41:35.770,0:41:39.970
"stackIndex" and "stackSet", I want, if I[br]call the "view" function, which is one of

0:41:39.970,0:41:45.020
the operations, I want the view function[br]to produce a consistent stack set. And

0:41:45.020,0:41:50.220
then it goes on to do all of that for all[br]the other ones. At the bottom here, you

0:41:50.220,0:41:53.929
can see some prerequisites that need to[br]hold for the property so that invariant

0:41:53.929,0:41:59.360
only needs to hold if the window, if the[br]number of the window is actually smaller

0:41:59.360,0:42:05.119
than the size of the stack set. Otherwise,[br]I think the function just returns what

0:42:05.119,0:42:09.850
would go with it, what went in there, So[br]that's a very, that's just a very

0:42:09.850,0:42:13.901
efficient way to invent properties, to[br]think of some invariant that shall hold in

0:42:13.901,0:42:17.490
your data structure. And if you know[br]Idris, you can sometimes encode that in

0:42:17.490,0:42:21.150
the types, but often that's kind of[br]tedious. And you can just write it down as

0:42:21.150,0:42:25.750
a property and then have QuickCheck check[br]it for you. And it's not particularly

0:42:25.750,0:42:29.790
exciting for the simple definition, but[br]you can imagine that the actual definition

0:42:29.790,0:42:33.710
when you have tiling window management[br]going on is much more complicated than the

0:42:33.710,0:42:38.420
one that you just saw. But you can keep[br]those same properties, right? There still

0:42:38.420,0:42:42.170
needs to be some consistency invariant[br]that, if you have tilings, the windows

0:42:42.170,0:42:46.150
don't overlap, and things like that. That[br]should be obvious. Write those properties

0:42:46.150,0:42:51.452
down, check them using QuickCheck and that[br]will weed out a lot of the bugs.

0:42:51.452,0:42:55.900
Here's an example from our[br]practice. We, couple months ago, we were

0:42:55.900,0:43:03.220
tasked with migrating a giant Visual Basic[br]6 application. It had a password checking

0:43:03.220,0:43:07.120
function there. You can see here a Visual[br]Basic 6 type signature. And the property

0:43:07.120,0:43:14.690
that we wrote was, well, if we create the[br]hash from the password and we compare it

0:43:14.690,0:43:19.590
with the hash that's in the database, then[br]they should all come out the same. And to

0:43:19.590,0:43:23.609
our surprise, that function, that test,[br]that property, failed when we ran it for

0:43:23.609,0:43:29.410
QuickCheck and we had to correct it[br]because that password hash is restricted

0:43:29.410,0:43:36.600
to 11 characters by some restriction in[br]the database schema. And so that means

0:43:36.600,0:43:40.330
that you can use QuickCheck not just to[br]sort of check the correctness of things

0:43:40.330,0:43:44.490
that you already know, but to actually[br]develop a model for what goes on in your

0:43:44.490,0:43:50.780
software, which you don't always know very[br]well. So that's what we did there. Another

0:43:50.780,0:43:57.090
example is, we wrote, for a large[br]industrial client, we needed to write a

0:43:57.090,0:44:01.200
synchronization application. So when you[br]had two mobile devices and they would sort

0:44:01.200,0:44:05.770
of meet as strangers, they would exchange[br]data and they all needed to look at the

0:44:05.770,0:44:10.940
same sort of device configuration data.[br]And we didn't want them to exchange all

0:44:10.940,0:44:15.230
the data every single time. We just wanted[br]to exchange them, the data blocks that the

0:44:15.230,0:44:20.840
other side was missing. And again, there's[br]great algorithms for this based on Merkle

0:44:20.840,0:44:24.470
trees. They're pretty complicated. You[br]have to do a lot of bit fiddling with

0:44:24.470,0:44:28.950
that. But fortunately, the property for[br]that is pretty easy to write. So here's

0:44:28.950,0:44:34.430
the property that says, well, so the[br]synchronization algorithm works on sets of

0:44:34.430,0:44:39.910
blocks, whatever a block is. So you can[br]see the property here for all pairs of

0:44:39.910,0:44:45.130
sets of blocks and more sets of blocks. So[br]they're called bs1 and bs2. Block set one

0:44:45.130,0:44:53.030
and block set two. What we can do is, we[br]want, if we union those two, then we get

0:44:53.030,0:44:57.270
all the blocks in the system. We call that[br]all, or we can call the synchronization

0:44:57.270,0:45:05.490
algorithm and that will give us two new[br]block sets, block set bs1' and bs2'. And

0:45:05.490,0:45:10.940
those block sets are the ones that get[br]transferred to the other side. OK. And the

0:45:10.940,0:45:16.150
criterion here just says if we take the[br]ones that we have, if we union them with

0:45:16.150,0:45:20.190
the ones that we get, we should get all of[br]them. That should be all of them. And that

0:45:20.190,0:45:24.530
should be the same for both sides. And[br]also, we want the algorithm to be

0:45:24.530,0:45:28.850
efficient so we don't want it to transfer[br]blocks. So we want to make sure that the

0:45:28.850,0:45:32.880
blocks that we have and the blocks that we[br]get are disjoint. That they don't have any

0:45:32.880,0:45:37.770
elements in common. Otherwise, we could[br]make that algorithm trivially correct by

0:45:37.770,0:45:42.420
just transferring all the blocks every[br]single time. And I can tell you, I

0:45:42.420,0:45:46.060
sweated. You know, I sweated one or two[br]weeks over this algorithm and it was

0:45:46.060,0:45:52.790
really hard to write. But this one test[br]weeded out all the bugs that I found along

0:45:52.790,0:45:58.730
the way. So that is just super, super[br]effective. John Hughes has a couple of

0:45:58.730,0:46:02.859
papers on hard bugs that he found. So he[br]found a bug in a distributed database

0:46:02.859,0:46:09.600
called mnesia. And that bug was dependent[br]on opening the database, closing it and

0:46:09.600,0:46:14.650
opening it again. So this is not the kind[br]of bug that you find by just writing a

0:46:14.650,0:46:19.710
bunch of smart unit tests. Right? So, if[br]you did anything shorter in the beginning,

0:46:19.710,0:46:24.980
so if you just open the file and then did[br]some lookups there, that would not

0:46:24.980,0:46:29.320
manifest the bug. You really needed to[br]close and then open again. Have you

0:46:29.320,0:46:33.830
turned, have you tried turning it off and[br]on again? But then the database breaks in

0:46:33.830,0:46:39.000
this case. And here's another example[br]called The Mysteries of Dropbox. So you

0:46:39.000,0:46:45.940
can imagine that with Dropbox you really[br]want certain properties to hold. Right?

0:46:45.940,0:46:50.030
And it turns out they didn't. They never[br]worried about writing properties down. But

0:46:50.030,0:46:54.700
John Hughes did it and found a couple of[br]bugs. So here's one. It's kind of hard to

0:46:54.700,0:47:00.711
read where it says client 1 writes a into[br]a file that was previously empty. So that

0:47:00.711,0:47:07.170
funky turnstile there is empty. So writes[br]a into a file and then deletes the file

0:47:07.170,0:47:12.220
and another client writes, replaces, sees[br]the a in the file replaces it with a b.

0:47:12.220,0:47:18.340
And then client 1 goes and writes c into[br]the file that it previously thought to be

0:47:18.340,0:47:23.190
empty. And then unfortunately, even though[br]you can imagine that you should see either

0:47:23.190,0:47:28.660
b or c in that file, but Dropbox deleted[br]it. So I think they fixed that bug now.

0:47:28.660,0:47:37.130
But. so you go. So it goes. Oscar Wikstrom[br]has a couple of great, pretty recent blog

0:47:37.130,0:47:44.740
posts on properties in a screencasts[br]editor that I highly recommend. So this is

0:47:44.740,0:47:51.200
a great tool for finding bugs, but it's[br]not the same as having a proof. Right? So,

0:47:51.200,0:47:56.150
you can still imagine that you can find[br]very subtle bugs that are not covered by

0:47:56.150,0:48:00.040
QuickCheck. QuickCheck just randomizes,[br]just generates randomized tests. So, that

0:48:00.040,0:48:06.510
is not the same thing as making sure that[br]there aren't any bugs. So the great thing

0:48:06.510,0:48:10.960
about Idris and the reason I chose it for[br]this talk is that Idris allows you to not

0:48:10.960,0:48:15.530
just encode properties in the language. It[br]also allows you to encode proofs in the

0:48:15.530,0:48:20.720
language. So here is the associative[br]property for the list concatenation

0:48:20.720,0:48:24.640
operation. And if you look at the top that[br]has the definition of that function from

0:48:24.640,0:48:30.100
the Idris standard library, it says ++, in[br]goes a list, in goes another list, out

0:48:30.100,0:48:35.730
comes a list. Then it says, well, if you[br]concatenate the empty list with any list,

0:48:35.730,0:48:41.080
that is just that list "right". Do you[br]see that? The second one says, well, if we

0:48:41.080,0:48:45.510
concatenate a list that starts with the[br]element x and goes on with xs, then we

0:48:45.510,0:48:50.830
just sort of pull the x in front and[br]concatenate the rest with "right". So

0:48:50.830,0:48:54.890
that's a classic recursive definition of[br]list concatenation in functional

0:48:54.890,0:48:59.060
programming. And now here's something[br]really strange in Idris. Here's the type

0:48:59.060,0:49:04.010
declaration for a definition, again in the[br]standard library, called appendAssoc. And

0:49:04.010,0:49:09.180
it says, if you have a list a, you have a[br]list b, and you have a list c, and in the

0:49:09.180,0:49:14.960
type it says, oh, the associative property[br]should hold. Right. And so this is a

0:49:14.960,0:49:20.980
statement of that property. That's[br]wonderful. It's not the same as a proof.

0:49:20.980,0:49:29.690
So, but writing proofs, who loved that in[br]math? Oh. Oh, you're good! I didn't. I'm

0:49:29.690,0:49:33.900
sorry. So. So the great thing about Idris[br]is, it helps you write down the proofs.

0:49:33.900,0:49:38.730
I'll show you how that works just really,[br]really briefly. So here's that. So here's

0:49:38.730,0:49:42.690
just what I showed you on that slide. So I[br]can load that in there and it says, well,

0:49:42.690,0:49:46.560
you're not done. You didn't write a proof[br]for that property, but in Idris, you can

0:49:46.560,0:49:50.900
just push a bunch of buttons. Now, I love[br]that. So I can push one button and it

0:49:50.900,0:49:55.360
says, oh, well, you should write a proof[br]of that form. You have lists a, b and c.

0:49:55.360,0:49:59.380
Well, now and I can push another button[br]that says, well, you're doing this on

0:49:59.380,0:50:04.800
lists and if you're writing anything on[br]lists, you always need to distinguish

0:50:04.800,0:50:09.000
between the two cases of the empty list[br]and the list that consists of the first

0:50:09.000,0:50:14.590
element x and further element xs. And then[br]it says, well, write down something, but

0:50:14.590,0:50:18.710
then I can tell Idris: Well, I'm too lazy.[br]I'm not going to write anything so I can

0:50:18.710,0:50:23.060
just push a button. And Idris wrote this[br]so you can see me, but I didn't type this

0:50:23.060,0:50:29.359
right. I just pushed a button and it says,[br]Refl. What is Refl? What could that be?

0:50:29.359,0:50:35.810
Well, you can ask it what Refl is. It says[br]Refl. Oh, you can see here, landing here.

0:50:35.810,0:50:39.530
Refl is just a proof sort of a built in[br]proof that says that if two things are

0:50:39.530,0:50:44.720
true, two things are equal, if they're[br]identical, if they're the same. Right. And

0:50:44.720,0:50:48.590
that kind of makes sense in the first[br]equation, because the first equation of

0:50:48.590,0:50:53.420
appendAssoc corresponds to the first[br]equation of ++. Can you see that, how it

0:50:53.420,0:51:01.420
corresponds? Can you see that? The first[br]list is empty. Can you see that? Can you

0:51:01.420,0:51:05.180
see how the first list is empty with the[br]first equation of appendAssoc and the

0:51:05.180,0:51:13.700
first list is empty up there with ++. Can[br]you see that? OK. And then it just says,

0:51:13.700,0:51:18.501
well, then obviously. Well, not quite[br]obviously, but then sort of the the way

0:51:18.501,0:51:22.650
that the definition works, it comes out[br]just right. So what's really important is

0:51:22.650,0:51:27.740
that Idris accepts that proof with the[br]first. The second one is slightly more

0:51:27.740,0:51:35.960
tricky. But again, we can get help because[br]we know that appendAssoc is this recursive

0:51:35.960,0:51:39.480
function. It recurses on the first[br]argument. So we're just going to do the

0:51:39.480,0:51:47.281
same thing in the proof. And you can tell[br]Idris that it should use that, that it

0:51:47.281,0:51:52.440
should use that fact, if you will. So[br]here's the recursive call. And again, I'm

0:51:52.440,0:51:56.440
too lazy to push a button. But if I push[br]that button, it also puts in Refl and

0:51:56.440,0:52:02.260
there's loads. So this it might be a[br]mystery to you how it works, but this is a

0:52:02.260,0:52:06.980
proof of the associate of property of the[br]list concatenation in Idris. And since

0:52:06.980,0:52:12.190
Idris helps you write it, it's kind of fun[br]to do that. Oddly enough, even for

0:52:12.190,0:52:16.090
somebody who doesn't, usually who doesn't[br]usually doesn't enjoy proofs. So the way

0:52:16.090,0:52:22.070
that you program in Idris, we haven't done[br]that a lot in this talk, is that you put a

0:52:22.070,0:52:26.280
lot of information in the types and the[br]more information you put in the types, the

0:52:26.280,0:52:30.320
better Idris will get at figuring out the[br]correct definition. And you don't have to

0:52:30.320,0:52:38.890
do it by yourself. OK. So that's really[br]nice. OK. So we got that and and sort of

0:52:38.890,0:52:43.790
these kinds of proof assisting systems[br]such as Idris have been used in a lot of

0:52:43.790,0:52:48.990
real world systems. One one prominent[br]example is SEL4, a version of the L4

0:52:48.990,0:52:52.810
micro kernel, has a long history, but[br]important properties of that kernel have

0:52:52.810,0:52:57.410
been verified. It runs in the security[br]enclave on iOS and even though it's

0:52:57.410,0:53:01.280
written in C, it provably does not have[br]buffer overflows or a lot of the nasty

0:53:01.280,0:53:06.161
things that are responsible for a lot of[br]security exploits. Compcert is another

0:53:06.161,0:53:11.310
example, which is a verified, I should[br]mention this has been verified with the

0:53:11.310,0:53:15.690
help of a tool called Isabel. Also, great[br]fun to use. There's a project called

0:53:15.690,0:53:20.390
called Compcert, which is a verified C[br]compiler, which is important for a lot of

0:53:20.390,0:53:24.360
certified software where, you know, the[br]source code might be certified. But how do

0:53:24.360,0:53:29.610
you know that the compiler generates[br]correct code? And you know, because it's

0:53:29.610,0:53:34.430
been proven to be correct. And even there,[br]you can shoot, you can cheat sometimes. So

0:53:34.430,0:53:38.050
for example, register allocators, very[br]complicated, very hard to prove right.

0:53:38.050,0:53:41.710
But what you can do is you can write a[br]checker that the register allocator did

0:53:41.710,0:53:47.810
its job, did its job well and you can[br]verify the checker. And so you can cheat a

0:53:47.810,0:53:52.150
bit. So there's tools for that. We've seen[br]Idris and there's a number of other tools

0:53:52.150,0:53:56.510
and they're getting more and more mature.[br]And they're great fun, really. They really

0:53:56.510,0:54:01.540
are great fun. But, you know, going back,[br]switching down a gear a little bit,

0:54:01.540,0:54:05.130
there's lots of useful properties that you[br]can look for in your programs. So

0:54:05.130,0:54:09.970
commutativity might be useful that you can[br]switch the two arguments for an operation.

0:54:09.970,0:54:13.790
Also, if you have relations, you might[br]remember that from some math class,

0:54:13.790,0:54:17.580
there's some properties here like[br]reflexivity, symmetry, antisymmetry and

0:54:17.580,0:54:24.320
transitivity. Reflexivity says that a is[br]always related to a. Symmetry says if it's

0:54:24.320,0:54:28.920
one way, if a and b are one way related,[br]they need to be related the other way too.

0:54:28.920,0:54:32.840
Antisymmetry intuitively would seem kind[br]of the opposite. That doesn't make sense.

0:54:32.840,0:54:38.770
It's just says: if two things are related[br]in both both ways around. So, for example,

0:54:38.770,0:54:43.369
you know, orders like less or equal are[br]antisymmetrical, then they must be the

0:54:43.369,0:54:47.820
same. And transitivity just says that you[br]can form chains of your relation. So those

0:54:47.820,0:54:53.260
are a little dictionary of useful[br]properties that you can look for. Let me

0:54:53.260,0:54:58.300
close with one fancy property that you've[br]probably seen somewhere and that property

0:54:58.300,0:55:03.810
is called Functor. And you might have seen[br]in your programing language, in your list

0:55:03.810,0:55:08.540
library or in your stream library. There's[br]a function called map, right? And you

0:55:08.540,0:55:13.910
know, even Java has that and has had it[br]for many years. And what map does is, if

0:55:13.910,0:55:18.670
you have some, you know, in Java, for[br]example, it says "Stream", or it might be

0:55:18.670,0:55:22.640
"List", right. It says, well, if I have a[br]list of As, I can apply a function to each

0:55:22.640,0:55:26.980
element of that list. But you can[br]generalize that, it doesn't have to be

0:55:26.980,0:55:31.190
lists. It could be an Optional of As, for[br]example. You could also apply a function

0:55:31.190,0:55:35.320
to the value that's in there. So, you can[br]generalize that notion, and then it's a

0:55:35.320,0:55:42.690
functor. And, of course, in Idris, you can[br]write down equations for functors. And,

0:55:42.690,0:55:47.660
please ignore the technicalities here,[br](stammers) but, if you sort of pick out

0:55:47.660,0:55:52.198
where it says "functorIdentity",[br]the middle row says g v equals to v,

0:55:52.198,0:55:56.000
which means g is the identity[br]function. When you feed in v, you always

0:55:56.000,0:56:00.640
get v back. And when you use map with the[br]identity function, you apply the identity

0:56:00.640,0:56:05.530
function on each element of your list or[br]whatever it is. Then then you always get

0:56:05.530,0:56:10.990
back the same list. And here just says you[br]get function composition. So if you apply

0:56:10.990,0:56:14.930
one function and then another function and[br]you do that either inside or outside the

0:56:14.930,0:56:18.490
map, you should also get the same results.[br]So there's also just as there is

0:56:18.490,0:56:24.230
associativity with monoids, with functors.[br]There's these laws and you might think,

0:56:24.230,0:56:27.999
well, where would I look for a functor?[br]I've never seen a functor except for the

0:56:27.999,0:56:31.959
ones on streams. A couple weeks ago in a[br]training, somebody said, well, you always

0:56:31.959,0:56:38.790
start with that animal example. Shouldn't[br]you look for a functor there? And I was

0:56:38.790,0:56:42.840
kind of, you know, sweat broke out on my[br]forehead, I was like, where's that gonna

0:56:42.840,0:56:47.330
go? But, we came up with this. So, if you[br]go back, you can see that this is obvious.

0:56:47.330,0:56:52.219
So, what you need for functors is, you[br]need a type parameter. Right. And so you

0:56:52.219,0:56:55.740
just look for a place to stick a type[br]parameter, any place here at all. And

0:56:55.740,0:56:59.439
if you look at Dillo and Parrot, they[br]both prominently have this weight thing.

0:56:59.439,0:57:03.200
Right. And so that seems more important[br]than the other two properties, which are

0:57:03.200,0:57:09.589
specific to particular kind of animal. And[br]so the weight, the thing to do is just to,

0:57:09.589,0:57:14.060
well, you can see I replaced upper case[br]Weight by lower case weight and made that

0:57:14.060,0:57:19.810
into a type parameter, and, I can then[br]provide a functor implementation down

0:57:19.810,0:57:23.581
there. And you might think, what is that[br]good for? Well, I don't know. Well, one

0:57:23.581,0:57:27.110
thing that you could do is you could[br]provide a different representation for

0:57:27.110,0:57:31.073
weights. Another thing that you could do,[br]if you look at the type for runOverAnimal,

0:57:31.073,0:57:35.820
it says animal weight -&gt; animal weight and[br]weight is a type variable. What that type

0:57:35.820,0:57:41.120
signature tells you is that runOverAnimal[br]does not know what weight is. And that

0:57:41.120,0:57:45.630
means that the weight cannot change as a[br]result of that function. And you see that

0:57:45.630,0:57:49.650
in the type signature you get immediate,[br]small benefit, but you get a benefit even

0:57:49.650,0:57:55.590
with silly examples such as this one. And[br]that really brings me to the end. So in

0:57:55.590,0:58:00.480
your software, in your domain model, look[br]for a Combinator, look for a function that

0:58:00.480,0:58:05.800
will combine two things into a bigger[br]thing. See if you can make that thing

0:58:05.800,0:58:09.609
associative and look for a neutral[br]element. And very often you will find one;

0:58:09.609,0:58:13.490
make it a monoid, you know, say monoid a[br]couple of times. You'll remember it.

0:58:13.490,0:58:17.461
You'll remember it. Generally, write[br]properties for the things, for the

0:58:17.461,0:58:23.390
operations in your software, test those[br]properties using QuickCheck. You know, if

0:58:23.390,0:58:27.770
you feel like you have a lot of time,[br]prove them correct. Find the functor. If

0:58:27.770,0:58:32.390
you found, if you found the monoid, you[br]know, find the functor next. You know, and

0:58:32.390,0:58:35.960
it takes, it might take time. I'm[br]very old. As you noticed at the beginning.

0:58:35.960,0:58:42.190
So. So it gets easier over the years and[br]it will just seem like a regular staple of

0:58:42.190,0:58:47.100
your of your arsenal when you program. And[br]of course, when the important properties

0:58:47.100,0:58:51.070
in your program have either been written[br]down, if they've been tested with

0:58:51.070,0:58:54.840
QuickCheck or even proven, then you can[br]sleep much more soundly than maybe you

0:58:54.840,0:59:04.820
currently can. Thank you very much.[br]<i>applause</i>

0:59:04.820,0:59:10.841
Herald: Thank you, Mike. So I see we have[br]three minutes for questions. Maybe that's

0:59:10.841,0:59:16.119
two or three questions. If you have any[br]come to the microphones, please. Do we

0:59:16.119,0:59:25.950
have a question from the Internet? No, not[br]yet. So, microphone two. Right.

0:59:25.950,0:59:34.050
Question: Hi. So, QuickCheck generated[br]hundred tests. Yes. What can we say about

0:59:34.050,0:59:38.580
the quality of this test? Could we say[br]your program was correct using thoese

0:59:38.580,0:59:42.561
tests? Are these tests good?[br]Answer: Yeah. Very good question. So what

0:59:42.561,0:59:46.380
would you say about the quality of the[br]tests? And indeed, if you really do serve

0:59:46.380,0:59:50.760
industrial strength applications, a quick[br]QuickCheck comes with a bunch of tools

0:59:50.760,0:59:54.880
that let you look, for example, at the[br]distribution of the individual example

0:59:54.880,1:00:02.250
rated and while you didn't quite see me do[br]that, but I mean, for your domain objects,

1:00:02.250,1:00:06.150
you will typically write generators that[br]will generate those examples and you can

1:00:06.150,1:00:09.990
reason about the distribution of those.[br]And you absolutely should do that because

1:00:09.990,1:00:15.420
otherwise you might miss large areas of[br]your test space. So, but there

1:00:15.420,1:00:20.390
are tools and they help you do that. But[br]even if you don't do that, you know, it's,

1:00:20.390,1:00:24.260
you find a lot of, I found a lot of[br]bugs in my software even without worrying

1:00:24.260,1:00:28.560
about that. But if you go beyond that,[br]look at the distribution thing.

1:00:28.560,1:00:34.360
Herald: Thank you, next one, please.[br]Number two.

1:00:34.360,1:00:40.660
Q: Let's say I've hacked a program, for[br]example, in Java or C# or whatever. How do

1:00:40.660,1:00:50.080
I, how do I apply what I learned so[br]far? So, where do I start when I have

1:00:50.080,1:00:57.690
already completed the C# program with,[br]yeah, how do I apply QuickCheck on that?

1:00:57.690,1:01:01.230
A: So, just pragmatically because it's[br]written in C#? That's the question?

1:01:01.230,1:01:03.720
Q: Yes[br]A: So, well, I have to be very concrete

1:01:03.720,1:01:07.839
here, I mean, so, if you can think[br]properties, right, one way to do, so,

1:01:07.839,1:01:14.790
for example, so, C# you can link with F#[br]and there is a QuickCheck version for F#

1:01:14.790,1:01:19.089
called "FsCheck". And FsCheck, actually,[br]even though it's itself written in F#, you

1:01:19.089,1:01:23.460
can also use it from C#. So, you have two[br]options. You can write your tests in a

1:01:23.460,1:01:28.491
slightly more awkward fashion in C#, or[br]you could just link your code with F# test

1:01:28.491,1:01:35.330
suite and write it down there. And there[br]is a fairly reasonable Java QuickCheck, I

1:01:35.330,1:01:39.530
hear. Another idea would be to use the[br]slightly more fancier, the slightly

1:01:39.530,1:01:45.150
fancier QuickChecks that exist for Scala[br]and Enclosure. I'm sure there's one for

1:01:45.150,1:01:49.220
Kotlin as well, and link that against your[br]Java code. Does that answer your question?

1:01:49.220,1:01:54.510
Q: So whatever language I use, I have to[br]find out what the correct implementation

1:01:54.510,1:01:56.890
of QuickCkeck?[br]A: Yeah. Yeah. But as I said, I mean

1:01:56.890,1:02:00.800
usually, a fun thing I do in training is,[br]I chat "QuickCheck" and somebody calls on

1:02:00.800,1:02:04.679
the language, you know. Quick, QuickCheck[br]PHP or something like that. And there is

1:02:04.679,1:02:07.989
one, sure enough, I didn't know about before.[br]Q: Thank you.

1:02:07.990,1:02:12.140
Herald: All right. Thank you. And thank[br]you, Mike, again, for showing us a way to

1:02:12.140,1:02:15.251
sleeping soundly.[br]A: Thank you.

1:02:15.251,1:02:20.649
<i>applause</i>

1:02:20.649,1:02:27.109
<i>postroll music</i>

1:02:27.109,1:02:45.600
Subtitles created by c3subtitles.de[br]in the year 2020. Join, and help us!