0:00:00.000,0:00:22.300
ChaosWest TV intro music
0:00:25.628,0:00:30.031
Herald: Good afternoon, everybody, and[br]welcome back to Chaos TV West.
0:00:31.267,0:00:36.614
We are going to see a prerecorded[br]talk by Michael Sperber
0:00:36.614,0:00:39.620
about mathematics for hackers.
0:00:39.620,0:00:45.313
Michael is… once was a mathematics[br]student, but never finished his degree
0:00:45.313,0:00:48.256
and is in the process of [br]revisiting this old love of his.
0:00:49.615,0:00:52.975
Dieser Vortrag wird auch [br]simultan übersetzt in Deutsch.
0:00:53.355,0:00:55.588
And, well, enjoy.
0:00:55.898,0:00:57.359
Michael Sperber: Welcome!
0:00:57.359,0:01:00.322
Well, I'm here to get you all [br]excited about math for hackers.
0:01:00.322,0:01:03.980
Now, you can have an entire hacker's [br]life without having encountered
0:01:03.980,0:01:08.520
much of mathematics. After all, this[br]conference and this community to a large
0:01:08.520,0:01:13.142
degree really is about finding unexpected[br]behavior in software such as Heartbleed.
0:01:13.142,0:01:17.797
I mean, there's zillions of examples, but[br]Heartbleed is an example where, you know,
0:01:17.797,0:01:22.164
the OpenSSL API exposed secret memory[br]through a regular API call. That was
0:01:22.164,0:01:27.710
certainly unexpected. Now, you might[br]consider this unexpected behavior to be
0:01:27.710,0:01:31.430
just an inevitable part of software[br]development because it's so complex,
0:01:31.430,0:01:35.270
right? Things that you didn't expect[br]happen due to all the complications and
0:01:35.270,0:01:40.090
the complexity. On the other hand, with[br]critical infrastructure, such as OpenSSL,
0:01:40.090,0:01:45.660
you really want certain aspects of that to[br]really run reliably, correctly. And so
0:01:45.660,0:01:49.497
really, that unexpected behavior comes[br]down to a correctness issue. And,
0:01:49.497,0:01:53.747
of course, that's where mathematics might[br]come in because mathematics deals in
0:01:53.747,0:01:59.369
correctness a lot of the time in the form[br]of proofs. Now, you can certainly apply
0:01:59.369,0:02:06.049
proofs to software systems to great[br]benefit. But of course, proofs are often
0:02:06.049,0:02:10.678
tedious and a lot of work. They involve a[br]great deal of mathematical intuition.
0:02:10.678,0:02:14.292
You might not feel like that today, and[br]you don't have to, because I will talk
0:02:14.292,0:02:19.640
about something else today. I will instead[br]talk about mathematics as a language.
0:02:19.640,0:02:23.005
Right. This is not a new idea, [br]it's hundreds of years old.
0:02:23.005,0:02:26.397
Here's a quote from Galileo [br]that said, well,
0:02:26.397,0:02:31.731
the world really can only be understood [br]in terms of the language of mathematics.
0:02:31.731,0:02:35.320
And, you know, a lot of [br]mathematics concerns itself with finding
0:02:35.320,0:02:39.980
formal methods for the world around us.[br]Now I want to emphasize the fact that
0:02:39.980,0:02:44.666
really mathematics doesn't really model[br]the world around us directly. It really
0:02:44.666,0:02:47.091
does that through the detour through our[br]perception, right?
0:02:47.091,0:02:51.045
Mathematics really is [br]a fundamentally human construct
0:02:51.045,0:02:55.000
that our mind uses to understand [br]the world around us.
0:02:55.000,0:02:59.270
And in that way, it's also a social[br]construct because, well, we don't really
0:02:59.270,0:03:03.885
need mathematics, if not for communication[br]between different people.
0:03:03.885,0:03:09.584
And that's really where, you know, the[br]value of mathematics for software comes in
0:03:09.584,0:03:14.510
because software also is an image, sort of.[br]Our perceptions perceptions of the world
0:03:14.510,0:03:19.510
around us, a lot of the time. At least[br]useful software is. So, one particularly
0:03:19.510,0:03:24.250
useful part of mathematics for hackers,[br]for software construction, is, well, first
0:03:24.250,0:03:29.234
of all, the language of equations. And[br]here's a couple of equations, right?
0:03:29.234,0:03:33.378
x plus two equals six, that's very simple,[br]specifies the value for x.
0:03:33.378,0:03:37.451
This next equation, well, it has... [br]so x is a variable
0:03:37.451,0:03:40.186
and the next equation has two variables, [br]has x and y.
0:03:40.186,0:03:44.190
So it has two x squared plus [br]two y minus two equals zero.
0:03:44.190,0:03:49.322
That's a quadratic equation. Might even[br]have, you know, several solutions. And
0:03:49.322,0:03:53.887
finally, there's an equation that involves[br]a function whose definition is unknown.
0:03:53.887,0:03:58.231
It just says, well, [br]f(5) plus f(7) equals 70.
0:03:58.231,0:04:01.026
Now, you know, [br]when it comes to functions,
0:04:01.026,0:04:04.060
well, those are things that also [br]exist in software. So we might
0:04:04.060,0:04:09.440
conceivably use the language of equations[br]involving functions to describe functions
0:04:09.440,0:04:13.500
in our software. So we might take that[br]equation to describe that piece of
0:04:13.500,0:04:17.651
software written over on the right-hand[br]side. And, well, you know, we could try to
0:04:17.651,0:04:22.250
kind of work through it. Right? You can[br]see there's a function, there's a variable
0:04:22.250,0:04:27.479
that's external to that function. So it[br]goes across several invocations of it,
0:04:27.479,0:04:29.860
called y. And it's initialized to 7.
0:04:29.860,0:04:34.163
And maybe if we call f(5), [br]x is going to be five.
0:04:34.163,0:04:36.740
Y'know, try to go through it in your mind.
0:04:36.740,0:04:41.140
z is going to stash [br]the old value of y, which is seven,
0:04:41.140,0:04:43.720
and then y is going to be set to x.
0:04:43.720,0:04:48.030
So it's not going to be five. And then we[br]multiply x with the old value of y, so we
0:04:48.030,0:04:53.175
multiply 5 with 7 getting 35. [br]So f(5) might return 35.
0:04:53.175,0:04:59.058
And with f(7), we then after that call f(7)[br]y is now 5,
0:04:59.058,0:05:03.661
we stash the old value[br]in z, so it's now 5
0:05:03.661,0:05:06.359
x is 7,[br]and it returns 35 again.
0:05:06.359,0:05:09.825
Only the product, the multiplication,[br]works in the other order.
0:05:09.825,0:05:13.773
And the sum of that is 70, so you might[br]say, well, that equation describes that
0:05:13.773,0:05:19.720
function over there. But really, we had to[br]go through a lot of detail and sort of
0:05:19.720,0:05:24.160
tracing through the program to figure that[br]out. And also, it only works with that
0:05:24.160,0:05:30.069
initial value of y and it only works if we[br]call those functions from left to right.
0:05:30.069,0:05:34.067
But the language of equation doesn't say[br]anything like that, that we really need to
0:05:34.067,0:05:38.430
respect order or something like that.[br]Really, f(5), in mathematics, should
0:05:38.430,0:05:43.040
always return the same value. Otherwise,[br]you know, it becomes much harder to really
0:05:43.040,0:05:47.840
consistently apply the language of[br]equations to programs. Therefore,
0:05:47.840,0:05:51.870
Really, that's I guess the first hint [br]that mathematics gives you,
0:05:51.870,0:05:55.750
is that you should write functions that[br]always return the same value given the
0:05:55.750,0:06:02.832
same input. But, I digress.[br]Another aspect of the language of
0:06:02.832,0:06:06.833
equations is a concept called[br]substitution, that you probably know. So
0:06:06.833,0:06:12.740
imagine that first equation says x equals[br]to 7. And then there's a formula that
0:06:12.740,0:06:16.890
has that variable occurring. And in the[br]context of that first equation, what we
0:06:16.890,0:06:22.040
can do is you can kind of plug in that[br]equation, we can substitute every
0:06:22.040,0:06:29.248
occurrence of x with the number 7 in[br]this case and then use that to figure out
0:06:29.248,0:06:33.480
the final result of that formula. That's[br]also something that fundamentally only
0:06:33.480,0:06:39.990
works, you know, if x doesn't change over[br]time. If your functions really return the
0:06:39.990,0:06:44.440
same value every time you call them with[br]the same input. Now, the substitution
0:06:44.440,0:06:50.228
principle is not just for equations of the[br]form where you say x is a certain number.
0:06:50.228,0:06:54.350
You might also have an equation that[br]expresses x in terms of another variable,
0:06:54.350,0:06:59.430
such as z in this case. And you know, that[br]first equation means, well, I can plug in
0:06:59.430,0:07:06.980
2z every time x occurs in that formula and[br]use that to do further evaluation or
0:07:06.980,0:07:11.550
simplification of that formula. And what's[br]more, it also works the other way around,
0:07:11.550,0:07:17.299
right? I can work. I can sort of read that[br]equation in the second line, also from
0:07:17.299,0:07:22.930
right to left. So order does not matter.[br]So that's a fundamental principle of a
0:07:22.930,0:07:27.370
branch of mathematical algebra, right,[br]that we have variables and that we have
0:07:27.370,0:07:32.510
that substitution principle and that we[br]have equations. So well, here's a well
0:07:32.510,0:07:37.724
known algebraic formula, the binomial[br]formula, or one of them, at least.
0:07:39.688,0:07:44.310
You might've learned that at high school.[br]But today I want to look at a couple of
0:07:44.310,0:07:50.831
more slightly more fundamental equations[br]that might be part might have been part of
0:07:50.831,0:07:55.879
your school algebra class. So I want to[br]point out that all of these equations have
0:07:55.879,0:07:59.457
names, and you might try to think of them[br]right now, but I'll try to go through them.
0:07:59.457,0:08:04.480
You might think of the names and[br]then I'll resolve when I'm done. So the
0:08:04.480,0:08:08.460
first equation says when you multiply[br]three numbers, it doesn't matter whether
0:08:08.460,0:08:12.120
you will first multiply the first and the[br]second one and then the result with the
0:08:12.120,0:08:17.652
third one, or whether you first multiply[br]the second and the third one and then
0:08:17.652,0:08:22.360
multiply with the first (I'm going from[br]right to left here). The second equation
0:08:22.360,0:08:27.210
says you can swap the two arguments of a[br]multiplication, and the third one says
0:08:27.210,0:08:30.950
that you can kind of multiply out a sum in[br]the sense that,
0:08:30.950,0:08:35.779
when you have [br]a times the sum of b and c,
0:08:35.779,0:08:41.779
you can multiply a individually,[br]with each of the of the sums there.
0:08:41.779,0:08:45.560
Now here are the names:[br]The first one says, well, it doesn't
0:08:45.560,0:08:52.240
matter which way we associate the[br]multiplication with these three numbers,
0:08:52.240,0:08:54.319
so it's called "associativity".
0:08:54.319,0:09:00.122
The second one? Well, it comes [br]from a verb that says "to swap".
0:09:00.122,0:09:02.229
So it's called "commutativity".
0:09:02.229,0:09:06.557
And the third one is about distributing [br]a multiplication over an addition.
0:09:06.557,0:09:09.149
So it's called "distributivity".
0:09:09.149,0:09:14.130
And so these are all very valuable [br]and useful equations, but
0:09:14.130,0:09:17.015
really the most useful one is the first[br]one, associativity.
0:09:17.015,0:09:21.272
And associativity is something that [br]works not just for plus.
0:09:21.272,0:09:25.861
It also works for multiplication, [br]for example.
0:09:25.861,0:09:30.450
So really, when you talk about[br]associativity, you don't talk about it in
0:09:30.450,0:09:35.770
isolation. You have to say what operation[br]you mean is associative or is not
0:09:35.770,0:09:41.050
associative; in this case, "plus" or[br]"times". Moreover, associativity is
0:09:41.050,0:09:45.440
something that's not restricted to[br]numbers. So, for example, here are two
0:09:45.440,0:09:51.260
Boolean equations that specify[br]associativity for a Boolean "or" or "and",
0:09:51.260,0:09:55.860
so with the "or" operation you can take[br]three Boolean values, it doesn't matter
0:09:55.860,0:09:59.160
which way you "or" them up, [br]you always get the same result.
0:09:59.160,0:10:02.991
And the same works for[br]the Boolean "and" operation.
0:10:02.991,0:10:05.389
While these are kind of primitive values,
0:10:05.389,0:10:07.757
but you can also have [br]values that have structure.
0:10:07.757,0:10:11.352
So, for example, you might [br]program with a list data structure.
0:10:11.352,0:10:16.456
So you have a list with elements, [br]a1, a2, and so on, until aN.
0:10:16.456,0:10:22.973
And you might take two lists, where the[br]second one has elements b1, b2, ..., bm
0:10:22.973,0:10:27.611
and you concatenate them together. I[br]wrote this with that funny bow tie symbol
0:10:27.611,0:10:32.917
there, concatenation. So you concatenate [br]these two lists, and that operation,
0:10:32.917,0:10:38.805
that concatenates any two lists is, [br]if you think about it, also associative.
0:10:38.805,0:10:43.620
Now, what value does it have[br]to know that an operation is associative?
0:10:43.620,0:10:48.080
So here's a classic example where that's[br]valuable. One way to think about,
0:10:48.080,0:10:53.180
associativity as well: you can move the[br]parentheses around, right? And if you can
0:10:53.180,0:10:59.990
move the parentheses around, it doesn't[br]matter where they are. And that means that
0:10:59.990,0:11:04.080
you can leave them out entirely if you[br]have sort of a chain of the same kind of
0:11:04.080,0:11:09.670
operation. So imagine you have a large[br]parallel computation that's structured in
0:11:09.670,0:11:14.680
the following way: you have individual[br]computations a, b, c, d and so on until z,
0:11:14.680,0:11:18.490
and they're all independent of one[br]another. And to get the result of your
0:11:18.490,0:11:23.210
overall computation, you all combine them[br]with that operation that's written as that
0:11:23.210,0:11:28.250
black rhomboid. I'm just going to say[br]diamond from now. So the diamond
0:11:28.250,0:11:34.690
operation. And so the combination works[br]with a diamond operation. But if you know
0:11:34.690,0:11:39.010
that the diamond operation is associative,[br]it means you can sort of bunch up your
0:11:39.010,0:11:45.730
"abc"s any way that you like. And so, for[br]example, you might say, Well, if I've got
0:11:45.730,0:11:50.710
four machines working on this computation,[br]I can split my individual computations in
0:11:50.710,0:11:56.040
four bunches. Combine, you know, diamond,[br]the first bunch, the second bunch, the
0:11:56.040,0:12:00.150
third bunch and the fourth bunch, and then[br]combine the results of those and I get the
0:12:00.150,0:12:05.570
same results. It doesn't really matter if[br]it's five bunches or six or seven, or even
0:12:05.570,0:12:10.200
if it's irregular, right? And so that's[br]the freedom that associativity gives you
0:12:10.200,0:12:16.779
in distributing your computation. And[br]this, what what I just told you, this is a
0:12:16.779,0:12:21.130
classic big data abstraction for large[br]scale parallel computations called
0:12:21.130,0:12:28.279
MapReduce. But I really want to talk about[br]something more fundamental today, which is
0:12:28.279,0:12:32.970
how we think about the things that happen[br]in our software. So here is an excerpt
0:12:32.970,0:12:37.529
from the Java API documentation and ir[br]draws an oval, so it has to do with
0:12:37.529,0:12:44.481
graphics, with images. And you notice,[br]right the draw over operation, it has
0:12:44.481,0:12:50.540
returned type void and the documentation[br]there talks about it in terms of pixels.
0:12:50.540,0:12:58.149
Now, really, we think of an oval as this[br]thing, right, as an object or a shape or
0:12:58.149,0:13:02.310
something like that, right, as an entity[br]in its own right. But if you look at the
0:13:02.310,0:13:05.540
documentation there, you can see that[br]drawOval doesn't create an object that
0:13:05.540,0:13:11.779
corresponds to the notion or mind has of[br]an oval, right? It just flips the colors
0:13:11.779,0:13:18.300
of a bunch of pixels in some imagined[br]canvas that drawOval paints on. So that's
0:13:18.300,0:13:22.060
very different, right? And then the notion[br]of having a thing that's an oval is really
0:13:22.060,0:13:27.339
something that our mind reconstructs from[br]those pixels. But that gives us a very
0:13:27.339,0:13:32.920
limited sort of API for dealing with[br]images. And you can do that differently in
0:13:32.920,0:13:37.339
a way that that is amenable to algebra and[br]mathematics. And well, you can find that
0:13:37.339,0:13:42.730
in several places. One that's particularly[br]accessible is the Racket Image Teachpack
0:13:42.730,0:13:46.490
library that comes with the racket system.[br]So I put a download link down there,
0:13:46.490,0:13:51.871
generally a great system to play with. And[br]so this is how it works: Well, Racket is a
0:13:51.871,0:13:57.140
lisp like language, so the syntax works of[br]a different from Java or C in that when
0:13:57.140,0:14:02.560
you call a function, the parentheses go,[br]around the function call and the arguments
0:14:02.560,0:14:07.820
and the arguments are separated by white[br]space rather than commas. So first thing
0:14:07.820,0:14:12.010
is you call a function called circle, you[br]pass it three arguments: 50, solid, and
0:14:12.010,0:14:17.240
red, and it returns a red circle. Well, as[br]you might imagine. But really, I want you
0:14:17.240,0:14:23.380
to understand that it doesn't flip pixels[br]or something like that. It really returns
0:14:23.380,0:14:30.209
an object representing the circle. And[br]it's only the racket API that then
0:14:30.209,0:14:35.740
displays that object as an actual picture[br]that we can view. But it could also do
0:14:35.740,0:14:40.540
something else with that picture: save it[br]to a file, send it to somebody over the
0:14:40.540,0:14:47.310
network or something like that. So well,[br]first function returns a circle. Second
0:14:47.310,0:14:51.970
function is also square function that[br]returns a square. You can see I can put
0:14:51.970,0:14:56.350
something, I can put outline instead of[br]solid to say that I want just the outline
0:14:56.350,0:15:00.760
of a square or there's this blue star at[br]the bottom returned by the star function.
0:15:00.760,0:15:04.269
So these three functions are kind of[br]primitive in the way that they create
0:15:04.269,0:15:09.149
images out of thin air from a bunch of[br]numbers and strings. And here's another
0:15:09.149,0:15:15.740
such function called right triangle that[br]creates a triangle out of thin air. Now
0:15:15.740,0:15:20.540
there's three more operations here that[br]don't create something out of thin air. So
0:15:20.540,0:15:24.041
there's the rotate function, for example:[br]it takes an image. An existing image - it
0:15:24.041,0:15:28.200
has to exist before you call "rotate" and[br]rotates it, in this case by 10 degrees,
0:15:28.200,0:15:32.600
just a little bit. And then there's two[br]other functions, flip-vertical, which
0:15:32.600,0:15:36.730
flips an image vertically and flip-[br]horizontal, which flips it horizontally,
0:15:36.730,0:15:43.380
so creates a mirror image, if you will.[br]Now, these two functions, they transform
0:15:43.380,0:15:47.980
an image in some way. And what's important[br]to understand is an image object goes in
0:15:47.980,0:15:53.620
and they returned an image object also.[br]And that image object that's returned, you
0:15:53.620,0:15:59.300
can pass it to other operations. So, for[br]example, that's what happens here. You
0:15:59.300,0:16:04.460
can, for example, rotate that triangle[br]again, as we did on the slide before. And
0:16:04.460,0:16:07.940
you can pass that result, you can stick it[br]into flip-vertical to then flip the
0:16:07.940,0:16:14.220
rotated image. Now what you see here is[br]particular examples. So "what happens to
0:16:14.220,0:16:20.450
the triangle when you first rotate and[br]then flip?" But some of these things can
0:16:20.450,0:16:25.730
be generalized to general equations that[br]hold for all images. So here's two very
0:16:25.730,0:16:30.150
simple examples. The first one says, Well,[br]if I flip an image and I flip it again, I
0:16:30.150,0:16:35.579
get the same image out again. And then I[br]think hopefully plays to your visual
0:16:35.579,0:16:39.660
imagination or intuition. The second[br]equation says, Well, if you flip
0:16:39.660,0:16:43.529
horizontally and then vertically or you do[br]it the other way around your first flip
0:16:43.529,0:16:47.260
vertically and then horizontally, you get[br]the same result. And again that should
0:16:47.260,0:16:52.589
conform to your visual intuition. So those[br]are traditional equations that
0:16:52.589,0:17:00.170
characterize how images work and how image[br]construction works. And we can get some
0:17:00.170,0:17:05.750
particularly useful equations from these[br]three operations that are on this slide
0:17:05.750,0:17:10.750
here. Now what they do is, they don't just[br]take one image and output one image the
0:17:10.750,0:17:16.620
way that rotate and the flips do, but they[br]take two images each and return one image
0:17:16.620,0:17:21.120
that results from combining them. So the[br]first function, "beside", takes two images
0:17:21.120,0:17:26.709
and sticks them together horizontally,[br]gives you the resulting image. "above"
0:17:26.709,0:17:30.350
puts them above each other. Gives you the[br]result. An "overlay" puts them on top of
0:17:30.350,0:17:36.840
each other. And these are operations. You[br]know, they have the same form as "plus" or
0:17:36.840,0:17:42.970
list concatenation or multiplication or[br]"or" or "and" in the sense that "or" takes
0:17:42.970,0:17:46.799
two Booleans and returns a Boolean. "plus"[br]takes two numbers, returns a number.
0:17:46.799,0:17:51.320
"beside" takes two images, returns an[br]image. Same thing for "above" and
0:17:51.320,0:17:54.550
"overlay". And whenever you have that, you[br]have a function that takes two things and
0:17:54.550,0:17:59.220
returns one thing, you can think about[br]associativity and you should. And in fact,
0:17:59.220,0:18:04.160
these functions, if you kind of work again[br]for your visual intuition, you figure out
0:18:04.160,0:18:09.099
that "beside", "above" and "overlay" are[br]all associative operations. So, with
0:18:09.099,0:18:12.780
"overlay", for example, should be[br]especially intuitive and that if you have
0:18:12.780,0:18:16.190
three images on top of each other, it[br]should not matter whether you first kind
0:18:16.190,0:18:20.659
of staple the top ones together and then[br]the bottom one to the bottom, or whether
0:18:20.659,0:18:24.290
you first staple together the bottom two[br]and then put the top one on top. In each
0:18:24.290,0:18:33.739
case, you have layers in the same[br]sequence. Now what can you do knowing that
0:18:33.739,0:18:37.330
you have an associative operation? We[br]already talked about parallelization.
0:18:37.330,0:18:43.489
Generally, you can do optimizations based[br]on some of the other equations, for
0:18:43.489,0:18:47.109
example, the equation that says, "flip-[br]horizontal twice doesn't do anything". You
0:18:47.109,0:18:51.710
can use that to optimize, right? When you[br]see somebody doing a flip twice, you just
0:18:51.710,0:18:57.500
throw out those operations. You don't have[br]to compute the actual flip. You can also
0:18:57.500,0:19:01.940
imagine computations where you can cache[br]intermediate results in the same way that
0:19:01.940,0:19:07.369
you kind of process that parallel[br]computation in a tree-shape, and it gives
0:19:07.369,0:19:13.309
you great flexibility in that caching and[br]recombining the cached values. So you can
0:19:13.309,0:19:17.999
generally just use that for performance.[br]You could also turn those equations into
0:19:17.999,0:19:22.049
what's called property based testing.[br]Right. You could stick in random values
0:19:22.049,0:19:27.309
for the variables and test whether[br]equations are actually fulfilled. And that
0:19:27.309,0:19:31.360
might help you debug or ensure the[br]correctness of your library. And finally,
0:19:31.360,0:19:35.559
if you really need something to be[br]correct, then you could provide for the
0:19:35.559,0:19:40.559
proofs giving you added assurance using a[br]technique called induction, because you
0:19:40.559,0:19:45.220
combine two things into a thing that you[br]kind of have to walk that construction
0:19:45.220,0:19:50.590
backwards. But again, this talk is not[br]really concerned with proof so much. But
0:19:50.590,0:19:56.340
again, I mentioned that earlier, I really[br]want to talk about the modeling aspect
0:19:56.340,0:20:01.389
that this mathematical way of thinking[br]about it suggests, right? Again, remember
0:20:01.389,0:20:06.690
of the Java drawOval function that just[br]flips the color of a bunch of pixels. And
0:20:06.690,0:20:10.570
here is the picture. But really, we view[br]this picture - our minds views this
0:20:10.570,0:20:17.429
picture as a bunch of concentric circles,[br]and each circle is a thing in its own
0:20:17.429,0:20:25.059
right. Now, I don't know what's intuitive[br]to you, but apparently it was intuitive to
0:20:25.059,0:20:32.510
some people to create that first function[br]drawOval. And that mathematical intuition
0:20:32.510,0:20:37.159
really tells you, well, make pictures,[br]make images into objects and then create
0:20:37.159,0:20:44.429
abstractions based upon them. So we can[br]use mathematics to kind of create you
0:20:44.429,0:20:48.240
create equations after the fact. But[br]really, mathematics gives us great
0:20:48.240,0:20:52.940
suggestions as what the library, what the[br]API should look like in the first place
0:20:52.940,0:20:58.340
that. Well, I often see people doing[br]something else, so that intuition might
0:20:58.340,0:21:02.609
have something to do with that[br]mathematical understanding. So let me talk
0:21:02.609,0:21:06.859
a little bit more about that language of[br]mathematics. Now that we figured out the
0:21:06.859,0:21:12.720
importance of associativity or equations[br]in general. So, people working in algebra,
0:21:12.720,0:21:19.179
they always talk about structures that[br]have three pieces, right? One piece is a
0:21:19.179,0:21:25.619
mathematical set. So just a collection of[br]a bunch of things, of objects. Then they
0:21:25.619,0:21:29.570
have operations on those sets and then[br]they have equations involving those
0:21:29.570,0:21:33.279
operations. On the right hand side, you[br]can see what we know already. So we have
0:21:33.279,0:21:37.460
some set "M"; it could be anything, could[br]be Booleans, could be numbers, could be
0:21:37.460,0:21:41.580
images. And then you have an Operation[br]Diamond that combines two of those M's
0:21:41.580,0:21:47.039
into one M. We here's a little bit funny[br]notation, right? With a cross there. What
0:21:47.039,0:21:51.899
it says is there's two inputs right cross,[br]cross, cross for each input. And so the
0:21:51.899,0:21:56.450
diamond operation has one M as an input,[br]another M as an input. And then there's
0:21:56.450,0:22:02.259
the arrow and that says that there's also[br]an M as the output. And then finally,
0:22:02.259,0:22:06.360
there's that associativity equation that[br]we've already seen quite a few times
0:22:06.360,0:22:10.840
today. And those three things packaged up[br]together, the set and the operation on
0:22:10.840,0:22:16.299
that set (in this case just a single[br]operation) and equations (in this case,
0:22:16.299,0:22:20.289
associativity), this is all called a semi[br]group. There are other algebraic
0:22:20.289,0:22:25.679
structures that we'll see. Now this[br]translates directly to programing. Your
0:22:25.679,0:22:31.600
set "M" in mathematics might just be a type[br]in your program. And these semi groups, they
0:22:31.600,0:22:34.460
occur in lots of places. So all of those[br]things that we've already seen with
0:22:34.460,0:22:37.820
associativity, you could just kind of[br]shorten your language and say, all of
0:22:37.820,0:22:42.580
those things are semi groups. So, for[br]example, at the top, it says: if you take
0:22:42.580,0:22:47.140
the mathematical set of real numbers,[br](that's that funny "R", that hollow "R"),
0:22:47.140,0:22:53.690
the real numbers, with the plus operation,[br](it takes two numbers from the "R" set and
0:22:53.690,0:22:57.860
produces one number), of course, has[br]associativity and therefore it's a semi
0:22:57.860,0:23:04.220
group. Lists, with concatenation, fulfill[br]the associativity equation. Therefore,
0:23:04.220,0:23:08.899
they form a semi group. And, for example,[br]the "overlay" operation from the images,
0:23:08.899,0:23:14.489
just as "beside" and "above" do, has that[br]same shape, right? Combines two images
0:23:14.489,0:23:19.570
into one image and fulfills associativity,[br]Therefore, images and "overlay" form a
0:23:19.570,0:23:25.549
semi group. Now, a semi group is not the[br]only algebraic structure, but it's a
0:23:25.549,0:23:30.070
fairly humble one. It can't do a whole lot[br]and therefore kind of mathematicians build
0:23:30.070,0:23:34.979
up from them. They take a simple algebraic[br]structure and they add more operations or
0:23:34.979,0:23:38.929
something else to it. So, for example, the[br]next step up from a semi group is
0:23:38.929,0:23:46.429
something called a monoid. So you take a[br]semi group and you add something, and I'll
0:23:46.429,0:23:50.100
try to explain what that is. So again, you[br]have to set you have a binary operation,
0:23:50.100,0:23:55.261
that diamond operation. And you also say[br]that in that system, there has to be a
0:23:55.261,0:24:00.700
special element. And you have to know what[br]it is. And that element is called
0:24:00.700,0:24:05.509
"bottom". That's what that line says, you[br]know, that upside-down tee, that's what I
0:24:05.509,0:24:10.950
call "bottom". And it also has to be part[br]of that set M. And now, as usual because
0:24:10.950,0:24:15.700
every monoid is a semi group, the[br]associativity equation holds. And the
0:24:15.700,0:24:19.989
bottom line explains about the identity[br]element about the bottom element, where it
0:24:19.989,0:24:25.590
says, Well, if you use the diamond[br]operator to combine "a" with the identity
0:24:25.590,0:24:31.159
or identity with "a", you get back "a". In[br]German, you often use the word "neutral
0:24:31.159,0:24:37.529
element". So it's neutral with with[br]respect to the binary operation that you
0:24:37.529,0:24:42.429
have in your semi group. And hopefully[br]that appeals to your intuition as it does
0:24:42.429,0:24:47.690
to mine. And if you take an algebra class[br]at the university level, you might learn
0:24:47.690,0:24:52.669
about more involved algebraic structures,[br]such as groups and rings and fields. And
0:24:52.669,0:24:56.789
every time you go a step up, right, a[br]monoid is a semi group plus a neutral
0:24:56.789,0:25:02.820
element. A group is a monoid with even[br]more operations and more equations. A Ring
0:25:02.820,0:25:10.529
even involves a another operation and more[br]laws. Same thing for a field. So, you just
0:25:10.529,0:25:14.809
add a bunch of stuff as you go up the[br]ladder. But for hacking, really? For
0:25:14.809,0:25:19.580
computing, for writing software, the two[br]most important ones from that stack here
0:25:19.580,0:25:23.229
are semi group and monoid and you don't[br]really have to worry about the rest unless
0:25:23.229,0:25:28.509
you really write mathematically inclined[br]software that involves those algebraic
0:25:28.509,0:25:32.889
instructions. So we've seen a bunch of[br]semi groups. Have we seen a bunch of
0:25:32.889,0:25:36.210
monoids? Yeah. Well, essentially all the[br]semi groups that we've already seen are
0:25:36.210,0:25:42.729
also monoids. So for example, the plus[br]operation on the numbers; zero is the
0:25:42.729,0:25:46.410
identity there: you add zero to a number,[br]you get back that same number. With
0:25:46.410,0:25:51.580
multiplication, well you multiply a number[br]by one, you get back that same number. If
0:25:51.580,0:25:54.739
you have a list you concatenate with it[br]the empty list, doesn't matter whether
0:25:54.739,0:26:00.649
it's left or right, well, sure enough, you[br]get the same list. Now the bottom three
0:26:00.649,0:26:04.720
examples might look a little bit funny[br]because they suggest that there's an
0:26:04.720,0:26:09.999
identity for this those operations, but[br]they all are the empty image, so they're
0:26:09.999,0:26:16.009
invisible. And so that points that out to[br]you. And monoids - I can't really over
0:26:16.009,0:26:22.059
emphasize this - monoids are everywhere[br]around us. So, a well-known software
0:26:22.059,0:26:26.600
engineer asked me a while ago and said:[br]Well, your mathematical structure is all
0:26:26.600,0:26:32.019
good and well, but what about really[br]concrete software things? You know, we use
0:26:32.019,0:26:35.240
shopping carts. How could you possibly use[br]mathematical structure for a shopping
0:26:35.240,0:26:40.970
cart? Therefore as well, a shopping cart -[br]you might have a shopping cart associated
0:26:40.970,0:26:46.140
with your account at some shop. Right? But[br]on another day you might go shopping, you
0:26:46.140,0:26:51.889
forget to log into your account. But you[br]can usually still fill a shopping cart.
0:26:51.889,0:26:57.760
Now, once you checkout that shopping cart,[br]you buy the stuff in it, it will usually
0:26:57.760,0:27:01.210
ask you to log in. Now there's two[br]shopping carts, one inside your account
0:27:01.210,0:27:06.929
and the one that you just filled. They[br]have to be combined into one. And really,
0:27:06.929,0:27:10.229
it's worthwhile to think about what[br]properties that combination operation
0:27:10.229,0:27:15.539
should have. But there's many other[br]examplesfor monoids. I have some concrete
0:27:15.539,0:27:21.000
examples from applications that I've[br]worked on. A famous paper in functional
0:27:21.000,0:27:23.230
programing, for example, is about[br]financial contracts - sure ehough, they
0:27:23.230,0:27:29.260
form a monoid. Recently, I talked to a[br]company that makes configurable flower
0:27:29.260,0:27:33.109
bouquets, so you might have well, you[br]might combine two flowers, two sets of
0:27:33.109,0:27:37.589
flowers into one to form a bouquet. You[br]know, all kinds of things. Monoliths
0:27:37.589,0:27:43.940
really are everywhere around us. So much[br]that, my friend Conal Elliott has elevated
0:27:43.940,0:27:48.240
this to a general design principle,[br]whenever you write software for a
0:27:48.240,0:27:53.559
particular domain, you should look for[br]mathematical algebraic structure. And
0:27:53.559,0:27:56.940
because monoids are so common, one thing[br]that you can always try is look for binary
0:27:56.940,0:28:01.750
operation on your objects. Check of the[br]associative law holds. Look for an
0:28:01.750,0:28:08.419
identity. And if you don't find that[br]binary operation, OK, but it's not
0:28:08.419,0:28:12.960
associative, you know, that's maybe a sign[br]that you should try to make it
0:28:12.960,0:28:17.210
associative. Doesn't always work, but[br]frequently does. And and usually gives you
0:28:17.210,0:28:20.130
some improvement in the process. Same[br]thing for identity: If there isn't one,
0:28:20.130,0:28:25.469
you might make one up, trusting that you[br]might need it later. Conal calles this the
0:28:25.469,0:28:29.759
Tao check. Something that I really like.[br]It's whether the software model that
0:28:29.759,0:28:35.059
you're creating aligns with mathematics.[br]And that means, with the deeper structure
0:28:35.059,0:28:38.999
of the universe that humanity has[br]discovered in the hundreds of years that
0:28:38.999,0:28:44.070
were there before computing. Monoids are[br]also useful in differentiation from things
0:28:44.070,0:28:47.399
that are not monoids. So, for example, the[br]maximum operation that gives you the
0:28:47.399,0:28:51.509
bigger of two numbers does not form a[br]monoid. It gives you a semi group. It's
0:28:51.509,0:28:57.710
associative, but well, there's no[br]identity, right? Thinking about it, you
0:28:57.710,0:29:02.149
might think, well, but can't I take minus[br]infinity or something like that? But of
0:29:02.149,0:29:06.960
course, that's not a real number. But it[br]maybe gives you a hint as to how you could
0:29:06.960,0:29:11.869
complete that structure if you really need[br]a monoid. I'll get back to that in a
0:29:11.869,0:29:17.200
second, but first I want to talk about a[br]general principle in that, it's not just
0:29:17.200,0:29:22.229
discovering monoids in the domain of[br]objects around you, you can also construct
0:29:22.229,0:29:27.509
monoids systematically. Specifically, you[br]can create larger monoids out of smaller
0:29:27.509,0:29:31.539
ones. So this is probably the most[br]complicated slide that I have. So don't
0:29:31.539,0:29:35.249
worry, it'll be over in the second, but[br]we'll try to go through it line by line.
0:29:35.249,0:29:40.080
So imagine you have two momoids. The first[br]one is called M1, the second one is called
0:29:40.080,0:29:44.929
M2, and each has their own diamond[br]combination operation. The first one is
0:29:44.929,0:29:50.389
called Diamond 1, the second one is called[br]Diamond 2. The first one takes two M1s,
0:29:50.389,0:29:56.559
gives you back an M1. The second one takes[br]two M2s and gives you back an M2. Now,
0:29:56.559,0:30:03.169
using those two momoids, you can create a[br]larger monoid by taking pairs of elements
0:30:03.169,0:30:08.100
from M1 and M2. That's what those funny[br]cross means. It's something called the
0:30:08.100,0:30:13.969
Cartesian product; out of two sets, it[br]forms the set of pairs where there's one
0:30:13.969,0:30:19.430
from each of those two sets in there. And[br]in order to make that a monoid, we have to
0:30:19.430,0:30:23.649
define the binary operation. I'm just[br]going to call it diamond. You can see the
0:30:23.649,0:30:28.210
diamond is defined in such a way that one[br]pair out of M1 and M2 goes in, another pair
0:30:28.210,0:30:34.460
out of M1 and M2 goes in and it returns[br]another pair out of M1 and M2. And the way
0:30:34.460,0:30:39.940
it's defined is, you take two pairs and[br]you combine the first elements from both
0:30:39.940,0:30:45.239
pairs using the M1 monoid and the Diamond[br]one operation. And you combine the second
0:30:45.239,0:30:51.239
elements of both pairs using the diamond[br]operation from the M2 monoid. And sure
0:30:51.239,0:30:55.850
enough, that gives you an operation that's[br]associative. I didn't put that on the
0:30:55.850,0:30:59.479
slide, but it also gives you an identity[br]with a pair that consists of the
0:30:59.479,0:31:07.659
individual identities from M1 and M2. You[br]know, that works. Also, sometimes you have
0:31:07.659,0:31:12.860
a semi group lying around, but you really[br]need a monoid. I mean, a semi group that's
0:31:12.860,0:31:15.970
not a momoid, but you really need a[br]monoid. Here's a little construction that
0:31:15.970,0:31:21.330
will build a monoid from a semi group. So[br]again, we start with the set. We start
0:31:21.330,0:31:25.809
with a binary operation on that set called[br]diamond, and then we create another set
0:31:25.809,0:31:30.110
that I call M-bottom (again, that funny[br]upside-down tee that you see there). And
0:31:30.110,0:31:35.009
we create it by adding artificially one[br]new element to it, right? It can be in
0:31:35.009,0:31:44.659
there before. And then we define a new[br]operation, Diamond-bottom, that operates
0:31:44.659,0:31:50.409
on that set. And and we just define it in[br]such a way that,if either side of that
0:31:50.409,0:31:54.859
operation is the identity, the bottom[br]element, we just have it return the other
0:31:54.859,0:32:01.259
side. So, "a, Diamond-bottom, bottom"[br]returns, you "a", and the same thing the
0:32:01.259,0:32:07.370
other way around. And whenever that[br]operation is called on two things that are
0:32:07.370,0:32:12.529
not bottom, we just call the original[br]operation. And sure enough, that gives you
0:32:12.529,0:32:16.470
a monoid. [glitch] that the thing before,[br]the M before, was just a semi group, and
0:32:16.470,0:32:20.200
you might have seen that construction when[br]programing. So, for example, the Java
0:32:20.200,0:32:25.320
library has something called an option,[br]and that is exactly that. And again, when
0:32:25.320,0:32:29.249
you're defining abstractions like that,[br]the mathematical notion of the
0:32:29.249,0:32:34.169
mathematical equations can provide a guide[br]as to how that API should behave if it's
0:32:34.169,0:32:38.539
supposed to be reasonable. If you're still[br]bear with me and have a little bit of
0:32:38.539,0:32:44.529
patience left, here's another concept it's[br]a little bit more abstract called the
0:32:44.529,0:32:49.309
homomorphism. And that's useful and[br]thinking about APIs, at least APIs that
0:32:49.309,0:32:54.940
combine in this way via something like a[br]monoid. So look at the first equation: It
0:32:54.940,0:33:00.279
says, well, if you take an overlay of two[br]images, a and b, - more like this - right,
0:33:00.279,0:33:04.120
and you rotate it, that is the same as[br]taking one image, rotating it, take
0:33:04.120,0:33:10.049
another image, rotating it and slapping[br]them together after the fact. And what
0:33:10.049,0:33:15.109
that means is really, "rotate" here is[br]what's called a homomorphism that can kind
0:33:15.109,0:33:22.149
of slip inside the overlay operation. Or[br]another way to talk about it is, commutes
0:33:22.149,0:33:27.029
or can trade places with the overlay[br]operation in that, on the left hand side
0:33:27.029,0:33:31.269
of the equation, the rotate is outside and[br]the overlay is inside, and on the other
0:33:31.269,0:33:34.819
side of the equation, it's exactly the[br]other way around. With the next equation
0:33:34.819,0:33:38.909
there flip-vertical of beside, [noise[br]while indicating the flip], right, and
0:33:38.909,0:33:45.049
then the idea is, well, you flip one, you[br]flip one and then do "beside". That's
0:33:45.049,0:33:48.350
certainly eminently reasonable, but if you[br]think about it, it might depend on the
0:33:48.350,0:33:52.460
alignment that you choose for your images[br]as you put them side to side, right, you
0:33:52.460,0:33:57.589
might decide to align them by the top half[br]like this. And then you might come to the
0:33:57.589,0:34:01.940
conclusion that that equation does not[br]hold. So, but again, it provides a guide.
0:34:01.940,0:34:05.749
It probably should hold - you should[br]design the "beside" operation in such a
0:34:05.749,0:34:11.420
way that it works. Now the equation at the[br]bottom really does not work, right? There
0:34:11.420,0:34:19.339
it is. But if you have five minutes after[br]this talk, or even now, you might think
0:34:19.339,0:34:22.889
about an equation that's very similar to[br]that one, that does hold and that gives
0:34:22.889,0:34:29.480
you some insight. That's also a useful[br]notion when you're designing APIs. Here's
0:34:29.480,0:34:36.100
another useful notion in that, Well, with[br]images, there's the visual aspect, right,
0:34:36.100,0:34:39.730
that if you perceive images by looking at[br]a certain pair of coordinates and
0:34:39.730,0:34:45.200
perceiving a certain color. And that color[br]might be, you might represent it by a
0:34:45.200,0:34:49.490
value and that value might come from[br]different types. And that gives you
0:34:49.490,0:34:54.500
different notions of images. So, for[br]example, the image of bools well, so it
0:34:54.500,0:34:58.920
means each coordinate can only be on or[br]off, or black and white. So it gives you
0:34:58.920,0:35:02.800
black and white picture. The next one,[br]where there's just a number there might
0:35:02.800,0:35:12.640
give you some some notion of grayscale. Or[br]you would, of course, then as in the
0:35:12.640,0:35:16.340
bottom two examples, you could stick RGB[br]triples in there to give you arbitrary
0:35:16.340,0:35:20.230
colors or even an alpha channel or[br]something like that. So when you have a
0:35:20.230,0:35:25.310
type such as image that has a parameter,[br]very frequently you can add a little bit
0:35:25.310,0:35:29.430
of structure, what's called a map[br]operation that you might have seen (not
0:35:29.430,0:35:33.520
going to worry about the details there),[br]but you might get a structure called a
0:35:33.520,0:35:42.020
functor. And the word functor comes from a[br]particularly abstract branch of algebra
0:35:42.020,0:35:45.210
called category theory. But even, you[br]know, the mathematicians sometimes call
0:35:45.210,0:35:51.770
that abstract nonsense. But, despite the[br]term, it really is something that's very
0:35:51.770,0:35:56.830
useful and very insightful and it gives[br]you a lot of insight into the structure of
0:35:56.830,0:36:01.830
things. And category theory frequently[br]describes relationships between things
0:36:01.830,0:36:06.540
through diagrams that are quite beautiful.[br]So here's a characterization of the idea
0:36:06.540,0:36:14.580
of a monoid. You don't have to understand[br]the diagram, but maybe, after this and
0:36:14.580,0:36:18.110
after you've mastered monoids for a while,[br]you'll have look at category theory and
0:36:18.110,0:36:22.960
enjoy it. You get more complicated[br]diagrams such as this one in more involved
0:36:22.960,0:36:30.070
abstractions such as, I mentioned functor.[br]There's also the infamous monad and these
0:36:30.070,0:36:35.870
are things that are practical, eminently[br]practical for creating higher order and
0:36:35.870,0:36:41.070
generally higher level abstractions.[br]Again, not for this talk. That's a
0:36:41.070,0:36:46.870
different talk. But I hope I've instilled[br]in you the sense that mathematics, at
0:36:46.870,0:36:50.830
least this kind of simple mathematics, is[br]useful. If you felt that it hasn't been
0:36:50.830,0:36:55.290
simple, that it's been hard, I want to[br]point out that, well, it might be hard to
0:36:55.290,0:37:00.950
understand everything that's been on the[br]slides on this talk, but it's not due to
0:37:00.950,0:37:05.980
the fact that it's complicated. It's not.[br]There's not a lot of moving parts or
0:37:05.980,0:37:11.840
something like that, but it is abstract,[br]and the human mind needs some time. It
0:37:11.840,0:37:14.810
finds it difficult to deal with[br]abstraction, and therefore you might -
0:37:14.810,0:37:18.630
also, if you're interested in this stuff -[br]you might give your mind some time to get
0:37:18.630,0:37:22.870
adjusted to those mathematical concepts[br]and maybe look at it again a couple of
0:37:22.870,0:37:29.350
weeks. Just have a brief look. You know,[br]maybe look for a monoid or just a binary
0:37:29.350,0:37:34.090
operation, look for associativity and by[br]and by, that stuff will become more
0:37:34.090,0:37:38.600
familiar and commonplace to you, and[br]you'll find it easier to deal with it. And
0:37:38.600,0:37:42.770
once that happens, I think you'll find[br]that very satisfying. So that's pretty
0:37:42.770,0:37:48.910
much it. If you want to read up some more[br]detail on this, I put in four references
0:37:48.910,0:37:52.150
that are linked from the slides that you[br]hopefully download from somewhere. But you
0:37:52.150,0:37:59.560
can also just search for those titles and[br]you'll find those papers. So first one is
0:37:59.560,0:38:03.820
a paper by Brent Yorgey that really takes[br]that idea of using monoids to structure an
0:38:03.820,0:38:11.120
image library to the limit. That's just a[br]great paper. Then there's a book by Sandy
0:38:11.120,0:38:17.630
Maguire on algebra-driven design, applies[br]that idea to different practical settings.
0:38:17.630,0:38:22.330
Conal Elliot gave a great foundational[br]type talk on something called denotational
0:38:22.330,0:38:25.330
design. So that's a video. Also has a[br]paper, but I really recommend you look at
0:38:25.330,0:38:29.690
the video. And the classic paper that[br]introduced this notion of dealing with
0:38:29.690,0:38:33.900
images by combining them is by Peter[br]Henderson, something called functional
0:38:33.900,0:38:40.680
geometry. And I hope you'll enjoy looking[br]at that stuff as much as I will. And I
0:38:40.680,0:38:51.880
hope you enjoy the Congress. I hope to see[br]you around. Well, have a good time. Bye.
0:38:51.880,0:38:59.150
Herald: So thank you for this interesting[br]talk, Michael. And there are a few
0:38:59.150,0:39:04.610
questions from the internet already. And[br]for those who haven't asked questions yet,
0:39:04.610,0:39:13.020
if you use the hashtag #rc3cwtv on either[br]Twitter, Mastodon or the proper IRC
0:39:13.020,0:39:18.440
channel, we can still include them in this[br]Q&A. And the first question I would like
0:39:18.440,0:39:25.730
to ask you, Michael, is maybe a strange[br]one, but you mentioned this concept of
0:39:25.730,0:39:33.370
homomorphisms of the monoids. And I was[br]wondering whether we could do the reverse
0:39:33.370,0:39:40.010
rounds. Could could you use these[br]mathematics to visualize APIs?
0:39:40.010,0:39:49.190
Michael: That's an excellent question. So[br]let me think about it for a moment..., so
0:39:49.190,0:39:57.670
with a monoid... So yeah, so the answer[br]is, first of all, yes. So with the monoid,
0:39:57.670,0:40:02.290
one way to think about a monoid is not[br]just this abstract thing that's going on
0:40:02.290,0:40:08.480
right, but since, any value in the monoid,[br]can kind of be built up by this operation
0:40:08.480,0:40:14.090
that's sitting in the monoid, you could[br]also just represent a monoid not just by
0:40:14.090,0:40:22.601
some abstraction, but you can build what's[br]called a free structure, and that is tree
0:40:22.601,0:40:26.950
structured and that you could visualize.[br]So that's one half of the answer. And on
0:40:26.950,0:40:31.000
the last slide, I had to reference the[br]very first reference on a paper by Brent
0:40:31.000,0:40:36.520
Yorgey shows how that works. And it's[br]generally a paper on visualization. So
0:40:36.520,0:40:41.100
that would be one half of the answer. The[br]other half is that I remember one
0:40:41.100,0:40:45.400
industrial project that I've worked on[br]where people wanted - so there was kind of
0:40:45.400,0:40:50.870
a complicated data flow problem, and the[br]requirement of the customer was, well,
0:40:50.870,0:40:57.380
people want to assemble a configuration[br]for a scheduling problem in semiconductor
0:40:57.380,0:41:01.130
fabrication, if you will. And they said,[br]Well, we want we just want a bunch of
0:41:01.130,0:41:06.520
boxes and arrows, and people should be[br]able to arrange that visually to specify a
0:41:06.520,0:41:12.440
configuration. And we ended up looking for[br]the right formalism to do that. In fact,
0:41:12.440,0:41:17.150
there is one in category theory. And[br]category theory generally is diagrams, but
0:41:17.150,0:41:20.550
there is a concept in Category theory[br]which just happened to fit, and we found
0:41:20.550,0:41:29.070
it by going from the customer requirement[br]to the mathematics. And that gave us a
0:41:29.070,0:41:34.460
naturally and very pleasant and actually[br]mathematically precise visualization form
0:41:34.460,0:41:39.380
for that. So I'd argue it's a great tool[br]to think about visualization. Hope that
0:41:39.380,0:41:44.070
helps a little bit.[br]H: OK, so we can finally look forward to
0:41:44.070,0:41:48.960
this, this kind of Neuromancer-like[br]landscapes while hacking.
0:41:48.960,0:41:52.700
Michael: Well, yeah, it feels like that[br]sometimes, yes.
0:41:52.700,0:41:56.340
H: Another question was from a viewer who[br]had never seen such sexy algebra in their
0:41:56.340,0:42:01.820
life: Whether you're willing to submit a[br]proposal next year to go into a little
0:42:01.820,0:42:09.060
more in-depth continuation of this talk.[br]M: Sure. I'm very happy to.
0:42:09.060,0:42:14.080
H: That's a short answer to a relatively[br]long...
0:42:14.080,0:42:18.180
M: OK. Can't say you haven't been warned,[br]but yeah, I'll try.
0:42:18.180,0:42:24.840
H: Yeah, and also it needs to be accepted[br]by the content team, obviously. Another
0:42:24.840,0:42:29.350
question that is about something you said[br]you wouldn't talk about, and that is about
0:42:29.350,0:42:34.390
formal verification of algorithms M:[br]Yeah, but none the less might be useful
0:42:34.390,0:42:40.180
for the audience to know if they're[br]seeking formal verification for
0:42:40.180,0:42:43.700
algorhithms. What avenues you would[br]suggest to people, especially people
0:42:43.700,0:42:48.480
without much of a formal background in[br]mathematics, to start looking at, as in,
0:42:48.480,0:42:54.370
placed for further learning.[br]M: Yes. Yeah, that's that's an excellent
0:42:54.370,0:42:58.650
question. So I think one place that I'd[br]start with, and I think there have been
0:42:58.650,0:43:02.190
talks about this at earlier iterations the[br]of the Congress that I'm sure you can
0:43:02.190,0:43:06.860
find. There is, in fact, there's a new, if[br]you will, family of programing languages
0:43:06.860,0:43:11.410
that are based on strong types called[br]dependent types. And they're very
0:43:11.410,0:43:16.070
expressive and they allow you to express[br]mathematical properties. Now, in the old
0:43:16.070,0:43:20.480
days, we would write down a mathematical[br]property, of a program that we wanted to
0:43:20.480,0:43:25.450
have, and then we would use - if things[br]are good, we would use a proof assistant
0:43:25.450,0:43:31.031
to find the proof, and that would be a[br]very cumbersome process that you would
0:43:31.031,0:43:35.630
have to do. Now, with this new family of[br]programing languages, Idris and Agda are
0:43:35.630,0:43:42.910
two prominent examples, what you can do is[br]you can give the type and you can push a
0:43:42.910,0:43:46.130
button (essentially - it's not quite so[br]easy, but there's actually IDE support
0:43:46.130,0:43:50.050
where you can push a couple of buttons and[br]it will generate a program that has that
0:43:50.050,0:43:56.010
type). And that program is guaranteed to[br]be correct, right? Because with the
0:43:56.010,0:43:59.940
combination of the type and the program[br]itself, there is the proof right there
0:43:59.940,0:44:05.490
sitting there. And that, at least for[br]simpler things, takes away a lot of the
0:44:05.490,0:44:12.540
burden, at least at the burden of getting[br]into this kind of tool. It's still kind of
0:44:12.540,0:44:16.080
intricate work to put together more[br]complicated proofs, but to get into that
0:44:16.080,0:44:20.490
medium, it's just great fun and it's a[br]very satisfying activity. And you don't
0:44:20.490,0:44:23.150
have that impression that you sometimes[br]have with proof assistants that you're
0:44:23.150,0:44:28.260
kind of fiddling in the dark with a[br]screwdriver. So, it it's a concrete place
0:44:28.260,0:44:31.030
that you're looking for. I would I would[br]recommend looking at a programing language
0:44:31.030,0:44:35.090
called Idris and maybe look at some of the[br]Congress talks that we've had about in the
0:44:35.090,0:44:41.070
past.[br]H: Yeah. Having been to at least one of
0:44:41.070,0:44:45.830
those Congress talks, I also would ask a[br]follow up question to that: Does the new
0:44:45.830,0:44:51.730
typing capability that, for example, Rust[br]provides, rise to this level that you
0:44:51.730,0:44:55.320
mentioned with Idris and other languages,[br]or is that not advanced enough for that
0:44:55.320,0:44:58.600
yet?[br]M: I'm not an expert on rust. I haven't
0:44:58.600,0:45:05.540
seen IDE support on that level. I'm pretty[br]sure the type - I mean Rust has a type
0:45:05.540,0:45:10.450
system that has a specific kind of[br]expressive capability that allows you to
0:45:10.450,0:45:15.190
express memory safety. Right? And then[br]because, your type-correct program, if
0:45:15.190,0:45:18.550
you're not using the unsafe features, is[br]guaranteed, is kind of proven to be
0:45:18.550,0:45:27.030
correct and to adhere to those to those[br]memory safety criteria. But I have not
0:45:27.030,0:45:32.020
seen the general expressivity that[br]language is like Idris gives you in Rust.
0:45:32.020,0:45:39.420
Maybe there's a way to do it, but I'm I'm[br]reasonably confident it's not as practical
0:45:39.420,0:45:44.430
and not as easy to get into.[br]H: Yeah, and also it's very off-topic
0:45:44.430,0:45:48.940
since you said you wouldn't be talking[br]about this anyway right now. So we're sort
0:45:48.940,0:46:01.020
of veering. One of the other questions is,[br]will you be around in the 2D world
0:46:01.020,0:46:03.830
sometime to talk directly to people from[br]the audience?
0:46:03.830,0:46:09.870
M: Yeah, sure, we'll do that right after[br]the talk. Maybe after a little lunch
0:46:09.870,0:46:12.420
break.[br]H: And then what nickname will you be and
0:46:12.420,0:46:15.480
where will you be hanging out?[br]M: My Twitter handle, which was also being
0:46:15.480,0:46:21.050
called "sperbsen".[br]H: We have this 2D rc3 world, this kind of
0:46:21.050,0:46:26.710
online adventure thing where the people[br]visiting are walking around with their
0:46:26.710,0:46:31.260
avatars and, well you haven't been there[br]yet, I take it from your...
0:46:31.260,0:46:34.330
M: No, no, no. I have been there. I'm just[br]saying my avatar there has the same name
0:46:34.330,0:46:37.270
as my Twitter handle.[br]H: I'm sorry. I'm sorry for interrupting
0:46:37.270,0:46:40.300
you..[br]M: So it's called "sperbsen" "Sperber" was
0:46:40.300,0:46:44.340
not available anymore.[br]H: I apologize.
0:46:44.340,0:46:52.730
M: So I'll be there.[br]H: And I think this... There's another
0:46:52.730,0:46:58.720
question, and it's: Could something like a[br]Turing machine have been constructed with
0:46:58.720,0:47:06.750
the mathematics of 2000 years ago?[br]M: So I got to Turing machine and I got
0:47:06.750,0:47:08.640
mathematics as of two thousand years ago,[br]but I lost...
0:47:08.640,0:47:12.730
H: Could something like a Turing machine[br]be constructed with the mathematics of two
0:47:12.730,0:47:17.930
thousand years ago. This may be a bit of a[br]speculative question.
0:47:17.930,0:47:28.400
M: I don't see anything that wasn't there.[br]I don't see why not. I'm not 100 percent
0:47:28.400,0:47:34.670
sure what exactly the mathematics of 2000[br]years ago was, right. You know, my basic
0:47:34.670,0:47:40.320
knowledge goes back a couple of hundred[br]years, but the basic mechanism of a Turing
0:47:40.320,0:47:44.280
machine is very simple. It's not my[br]preferred mechanism to talk about
0:47:44.280,0:47:50.210
mathematics and hacking, but, sure, why[br]not?
0:47:50.210,0:47:58.160
H: And the, I think, final question is[br][...] start teaching Haskell in teaching?
0:47:58.160,0:48:02.970
M: Well, that's a great question. It kind[br]of goes, I'm doing a workshop later on
0:48:02.970,0:48:07.120
teaching programing. I think teaching[br]programing using Haskell is a terrible
0:48:07.120,0:48:14.510
idea. So obviously, you all know, I'm a[br]big fan of functional programming. I
0:48:14.510,0:48:17.780
actually do a lot of Haskell in my daily[br]life. and I've given talks using and on
0:48:17.780,0:48:21.540
Haskell in the past. But Haskell is a[br]programing language coming out of the
0:48:21.540,0:48:25.250
research community and used for[br]professional programing. If you really
0:48:25.250,0:48:29.170
want to do an effective introduction to[br]programing, you're well off using
0:48:29.170,0:48:33.500
specialized programing languages for[br]learning. That's what I will advocate
0:48:33.500,0:48:39.260
later today at 4pm Middle European Time.[br]H: OK, thank you. And this concludes the
0:48:39.260,0:48:48.460
session, thanks for being here.[br]M: Thank you. Thanks for having me.
0:48:48.460,0:49:06.460
postroll music
0:49:06.460,0:49:09.020
Subtitles created by c3subtitles.de[br]in the year 2021. Join, and help us!