Programming with Proofs - Computerphile

Key Takeaways

little bit of a cliffhanger on last time where we said about you know the idea of proofs program proofs where do we go from here then yes so we can use acta the programming language also to do proofs which which means i mean we can do a number of things we can prove mathematical theorems very exciting for some okay but for the programmer we can actually certify our programs we can prove that our program has certain properties right so i wanted to do a quite a simple problem so what i'm going to do is a problem about lists so i'm going to define an operation on lists which is called reverse and turns the list around yeah and what i want to prove is something maybe quite obvious namely if i turn a list around and then turn around again i end up with the list i started right lots of properties of programs you want to prove are actually quite simple intuitively clear you could say but to actually prove them and make sure that they really hold is actually still important because some of the properties you think intuitively are very clear about your program are alas completely wrong because you made just some stupid mistake some stupid error or whatever and it doesn't work but here we really have to prove some very stupid properties some you can see very from a mathematical point of view very trivial theorems but they better for us when we want to run the program point so here i i have set things up already have an acta buffer i've already put in my favorite list one two three okay and what i want to do is i want to do two things i want to define a function a reverse of f which gives me a list of a produce a list of a right and so the idea is that this function reverses a list okay we are going to do this in a moment but then once i have done this function i want to write another function and this i call ref and here is a type so reference as input gets a list of a and as output it produces a proof that if i reverse this list twice so i do left a's and then ref again i end up with the list i started and here i use a dependent type the equality type and that was featured in our recent video about martin hoffman's work so that's the idea so we first write the program and then we write another program and the second program actually tells us something about the first problem so how do we write ref okay f of some a's and now again how do i write ref i have to apply a magic trick oh is this this is vin guardium leviosa exactly basically recursion exactly so first of all i split my input it's either the empty list or coins list so if you reverse the empty list you get the empty list and here how do we reverse a cons list so if you think about if you reverse a list one two three the reverse of one two three should be three two one right so what we need to do is if we recursively reverse the list 2 3 we get the list 3 2 and then we put the first element at the end yeah so how do you reverse the console list you you take the tail you recursively reverse the tail and then you put your your beginning and the end yeah you put your head to your tail sort of yeah okay this means we need to have a way to put something at the end of a list so the cons puts things always in the beginning but now we have to put it at the end and here i have a name for this operation which is called snog why is this operation called snook oh i'm there tell me is it by chance reverse of cons very good well done so we have this operation snork which is cons backwards right and okay i'm going to write this in a minute i mean that's one way of how to do software development right i write my function and then discover i need some auxiliary function i just say okay okay i'll do this later first of all i do my function and then i go back and and fill in the details okay let's do it so here reverse we do what i state we reverse a's and then we snork a at the end okay so ref is sort of finished but not really because now we have to fill in snog how are we going to do snook what is the magic word recursion ah very good so it'll be curled me first of all split the list okay and if the list is just one element the output is just the list with with one element if i yeah if i snog an element at the end of the empty list i get a list just containing a and here okay that's the x i'm not going to replace the x by a because my other parameter is called x let's keep it as x um so what am i going to do if i put a at the end my list will begin with x again right but i have to snog my a at the end of ace okay so let's see let's see if i if i if i if i do this snork let's first test snog i say snog my favorite list and then i put four at the end i'm not very creative okay and we get that just works and now let's take let's test our f so ref of l1 is 321 works and you can also try exactly what happens test if you reverse l1 and then reverse it again we end up with a list from the beginning but okay now let's prove that that's always the case so we prove this by writing another program and this program is interesting it has a dependent type right we see here the arrow the input is a list a but we give it a name namely ace and the output is a proof and this proof depends on the input this is from the input occurs here okay before we start we need to understand what we can do with equality so let me just copy some lines some comments here so here's the definition of equality uh from the library so i say two things are equal the only way to to prove this is called raffle the raffle is a canonical proof of equality like zero and success or canonical natural numbers and using this idea i can prove some useful properties of equality so here's one i call tons for transitivity which is a function giving given a proof that a is equal to b and another proves that b equals to c it produces a proof that a equals to c now it's not difficult to write this program it's a one-liner because we only have to match the first input against raffle and i explain this a little bit in the video about martin hoffman here's another useful library function we need if we have a function from a to b and we know that the inputs are equal the outputs are also equal and it turns out again we can prove this by just pattern matching okay so this is already done in the library so now how do we prove reference how do we write this program magic word recursion very good okay so the pattern match on ace and so that is the first case is that a ref of wrath of nil is equal to nil now it turns out this is very easy because what is ref of wrath of nil ref of nil is nil and wrath of nil is nil so it must be there's nothing to be proved here they're just identical if you're looking actually in acta arcta tells us that the goal is to prove that nil is equal to nil because it has already calculated that the ref of wrath of nil is nil so all what you have to prove is nil is equal to nil and that's rifle okay very easy this case is not so easy so let me let me explain this a little bit what we want to prove it's down here let me just copy this we want to prove that f of f of x counts a's is the same as x cos a's now akta calculates this and it it evaluates the program as much as it can so it it says ref of x con something is the same as snork of graph i mean that is our definition of ref but now it's a bit stuck because it it doesn't know what is ref of snog but what is ref of snook if i reverse a list where i put an element at the end this element will move to the front right and the rest is reversed so what is ref of snog of x so this x moves to the front and the left moves inside so it's f of f of a's and now why is this one equal to x-cons a's now yeah because ref of a s is equal to a's this is just the recursive call to reference always prove this and we can recursively call ref to prove this thing okay so here we have to combine two equalities this one no actually this one and this one and combining equalities we use this trans program because if you have two equalities we put them together saying trans okay the first step is to move a snog over a ref into a cons all right so really what we want we want and we want a quality here namely that rf of snog axis a is equal to a cons graph of x's all right that's exactly the property we need and this is just another program it's i call it snog okay and now we have to we have to quantify all these things so we have a function which gets as input a list and an element and then prove this and here is the same situation that we have before when we wrote the program this is an auxiliary program and these auxiliary programs they are called lemmas in a meta mistake they are called lemmas in in mathematics so these are just auxiliary programs okay so what do we do we first call our ref snork refsnoc the first element is ace so if you look at this proof the first list here is the left of a so we have to tell it ref of ace and what's in the end is the x okay let me just make a bit of space and now the second thing is is sort of easy we just have to apply this ref ref as is equal to a's but we have to use this under the cons so here's a cons in front and that's exactly where we need this other operation maybe it's called com so we use the fact that cons preserves equality so so we use this function which uses a lambda which says basically that if you cons the same element in front of a list and two equal lists will produce two equal outputs and now let me put another shed in here oh it's not an a that's an x and there should be an x's okay so i open the shed and i have this other shed left and this is actually exactly what i want to prove but for a shorter list and here really we have to do recursive call okay so this is the proof that the ref that reversing twice is equal to its input but it uses this refs knock and okay i'm not going to complete this program or this proof actually uh it's two-liner it's not it's not difficult and it only uses what i've already introduced but i leave this as an exercise but what we see here is that we can write programs which prove properties about other programs and maybe you have noticed that there is that there are two magic words which turn out to be the same the one magic word is from programming recursion and there is another scary magic work for mathematics which is called induction and it turns out these two are the same because here we could really do a proof by induction but it is nothing else but recursion what we can do with this technology is a number of things so one thing is in academia when you write a mathematical papers or theoretical papers where there are theorems involved we can check that these theorems are really true by proving them formally and that's really quite a widespread nowadays already but they're also industrial applications and they're already starting to be used where uh some programs which are quite uh security sensitive or financially important uh are formally verified and they can be guaranteed that they have certain properties that's a lot of extra work and we are working on the technology to make it easier to do these proofs you know we want to make them more automatic need lots of help maybe use some machine learning to learn how to do them but in the end we want to have a program by whatever means it's produced which gives us a certificate that another program does its job canonical numbers for the numerals and here when we define construction on equality proofs it's enough to do this for the canonical one which is reflexivity which means i only have to you could view rgb as in some sense 3d so the first plane is r r g and b or vice versa