>> Hey, everyone. As much fun as ice cream is -- hey, ice cream, woo! We are going to start into the next and I think last round of talks. So please mosey on back to your seats. >> Hi, everyone. We're experiencing some minor technical difficulties, so we'll be live as soon as we can. >> Hello. Are you having a good !!Con? All right. And... I think that we all maybe want to thank Stripe for the ice cream. Thank you, Stripe! (applause) >> One small announcement is that, for those of you who have been listening to music either here in the space or on the stream, that was Creative Commons licensed music by Dr. Vox. Thank you very much, Dr. Vox. (applause) >> Due to minor temporary technical difficulties, we are switching the order of the first two talks in this session. This is the last talk block of !!Con 2014. And there will be four talks, and instead of the first talk being about brainwaves on your computer, that will be the second talk. And the first talk is proofs about programs, proofs as programs, and programs as proofs, by Katherine Ye. Please welcome Katherine Ye. (applause) >> All right. Hello, everyone. I'm Katherine, and I will be telling you about these three things. Proofs about programs, proofs as programs, and programs as proofs. And as a bonus, you will also learn why there is a giant rooster on this slide. So consider these two images. This is the -- the left one is from 1967. The right one is from today, basically. And it's not that important what the text says, but I want to kind of walk you through the development of -- hey, I wrote an entire paper about proving this compiler, versus -- hey, I used a computer to prove all of my transformations correct. So let's say you're a compiler. Great. So imagine being a compiler. And you get someone's code to look at and optimize. And so you see this strange piece of... This strange snippet of code inside that person's code, and you think -- well, this could probably be optimized. So it looks like this. And you think -- well, I don't really want to do the not operation. If I get rid of the not operation, and just switch end1 and end2, it'll save me time. It'll be the same. So you want to convince yourself that these two pieces of codes are equal. So let's just say for every input, the output is the same for the two pieces of code. So for all intents and purposes, they're equal, even though there might be mutation going on. So if you're here, you can probably already do the proof for yourself in your head, but I want to walk people through it, just to see if we're right or wrong about these two being equal. So actually, let's just think about it first. So this x less than c condition here can be true or false. Let's do a case analysis. If it's true, then great. If it's false, then great. It looks like they do return the same thing. So looking at the truth table, if you look down the true column, they both return end2. On the false column, they both return end1. So we've convinced ourselves that these two statements are equal. So this has an application in the real world. Compiler optimizations. Sometimes it's not this easy. You might have pointers or mutations or something, but when you just want to consider the simpler case, it'll generalize. So remember, you're still a compiler. All we did was convince our human selves on paper this was probably correct. We want a computer to check if we're actually correct. Here's where the rooster comes in. So Coq is an interactive theorem system. It's called Coq, because it was written by French people, and they love roosters. It's the national mascot. One great thing about Coq is according to category theorists, it's the world's best computer game. So you'll see we'll now prove that our code is the same. So do you guys need the font to be larger? >> Yes. >> Considerably. >> I actually don't know how to do that. >> Command plus. >> Good? Okay. Great. So... A quick refresher. We assert that these two are equal. Coq will prove -- we analyze the two cases. Don't worry about what this says. It's for later materials. So let's look at the actual set of the theorem. We assert that for all these variables, then basically exactly the same things... For the notation, the less than, just ignore the primes. They had to redefine some things. So great. I'm not going to talk while I'm doing this proof, so you guys can focus on reading it. So I know the text on the right is a bit small, but we will probably need the whole buffer for that. So... On the right, we have the state. Like, what we have introduced so far. And on the bottom is what we want to prove, currently. So we've got our first case done. The purple is checking that everything you've done so far is correct. And that's the video game aspect of it. >> Ooh! >> So great. Everything is... From the context. Which means that we can write every mathematician's favorite word here, and it works. We've proven it. Great! (applause) >> So yes, that was our interlude. So the first time I saw this, my mind was blown. And I wanted to know what is actually going on behind the scenes. What is the internal representation of the math inside? How does it know how to simplify things or check that -- oh, this had this condition, so I can just simplify it to end1 or whatever. So let's take a look at the internals, briefly. How does Coq work? First, the name is based on CoC, and CoC stands for calculus of constructions. Don't worry too much about what that is. It's a generalization of a correspondence that we want to talk about here. So this correspondence... Well, there's an interesting way that you can interpret your proofs as programs. And your programs as proofs. So let's talk about kind of the most well known part of this, or the most general part. So we have a type corresponds to a proposition. I'm using corresponds to in kind of a colloquial, non-rigorous way, so think of it as -- you have a one to one correspondence. Can match each one, and one set with each one and another set, and the function that does this preserves the structure in some way. So let's consider a type. A to a. So this means if you know about Haskell, you'll be familiar with this. If not, it means it's a function that takes something with a type a and returns something with a type a. Maybe your function takes 3 and just returns 3 or something, so it would be from int to int. So one kind of function that might live inside this type would be, say, if I just -- if you gave me something of type a, and I always return the same thing of type a, then clearly that does that, and this function is inhabited, or something lives inside of it. So great. Let's just say we have the identity function. And on the other hand, how are we going to interpret this as a proposition? So proposition in math terms -- or actually, in more colloquial terms, is, if you have a bunch of hypotheses, and you want to have some kind of ending goal -- so one proposition might be if it's raining outside, then I will get wet. That's one thing. And so if you'll interpret arrows here as implication, then you would say... If a is true, then a is true. Or if a, then a. So great. We basically have a corresponding proposition for this type. This is possibly a very simple example of the existing work. So considering a more specific example, inside this a to a, we have something that lives inside it. A program actually does that. That's the fx equals x. Similarly, for a to a, we have a proof that lives inside it, and it's just kind of like tautology. Like, we assume a is true, so it's true. Great. So let's actually inspect our own code. And see kind of what it looks like. Sorry about it being small. But yes. So over here, we have our proof in a kind of tactic language that Coq has to make things easy, and on the right is the interpretation in Gallina, which is what it looks like in Coq's internals, and it's a language very similar to ML, so you can actually see function -- some arguments, natural number, and then some expressions that return things. So it's great. There's a proof embedded inside it. Some possible future directions, if you're interested in this -- oh, by the way, yes, the fancy name is the Curry-Howard isomorphism. I didn't want to say it at first, because I didn't want to scare anyone off, but yes, there's future work here. I would love to do a talk about each of these, maybe, but I have 23 seconds left, so... Yes. The most interesting application of Coq is that... Not application, but implication is that it's based on this interesting new kind of mathematics, and you should check out homotopy type theory. And I would like to assert that the most important application of Coq is writing the game 2048, which exists... And let me show you that first. Huh. Okay. I can actually show people who come up to me later, but it's great. You have this statement that says there exists a sequence of moves such that 2048 is solvable. And then your proof is a sequence of moves, like left, right, up, down, and once you've gotten to 2048, you can say QED, and it'll complete. So that's very clear -- it's not a perfect example of Curry-Howard, but it's kind of an example of how a proof can be a program. Thanks. (applause)