Scale By The Bay 2019: Bill Venners, In Types We Trust

Recording: Scale By The Bay 2019: Bill Venners, In Types We Trust

I have just one idea that I would like to propose and then feel free to come up to me afterwards and give me your opinion and I'm gonna start with a page of eiffel code this is the eiffel programming language to illustrate something that Bertrand Meyer the guy who invented eiffel calls designed by contract this was a programming language that came out about the same time C++ came out and competed with C++ for mindshare and lost pretty much to C++ but he had the idea of that you would not just implement a function but also specify and test the behavior of the function all kind of together in the in the same source code so they do part of the function there the middle part is the actual algorithm of square root then there's these two other things require and ensure and require he called a precondition and he said that that is a part of the contract of this function that is the responsibility of the caller so it's not your fault as the implementer of the function if X is less than or equal to or less than zero and you're you you you it's the fault of the caller and that's a their bug and this functions gonna throw an exception so that that is an assertion essentially that was you know expressed in the code as part of the contract that specification is function and then at the bottom there's an insurer clause which is a a post condition he called it and a post condition is also an assertion that says what what you as the implementer of this function are supposed to do so that's what your responsibility is so that's the called design by contract and the idea was that assertions would run when the program runs so like little tests that run as the program runs by default require clauses are enabled and ensure clauses are off in Eiffel and that's kind of what we did in in the java community so this didn't take off this language really did take off that much and C++ sort of one out and he did not have this did not have designed by contract and Java came along and it also did not have designed by contract so in Java what we do is we express the contract of a function mostly in English so we do check preconditions and we don't turn them off and skal there's a nice pre-death called require method and predefined where we can kind of very nicely say this square root function requires certain preconditions that's the responsibility the caller if the caller doesn't fulfill their obligation we reward that caller with exception right illegal our get exception and then the rest of the contract is stated in English saying this is what the things supposed to do anybody who reads this method with another algorithm in a subtype someday would need to fulfill that contract so that's the same concept but it's not in code anymore it's in English or some human language and then what we did is we moved the postconditions over to this other completely different area called the tests and what did actually take off and at least the java marketplace of ideas was tests to have test-driven development this was well marketed by Kent Beck and Eric gamma the two guys that created j-unit so this really took off in the java community and so what we do is we do tests off to the side and this one is called example based tests because i just pick certain examples and try my function to make sure it fulfills its contract that was expressed in english and the idea of TDD is you'll write a little test implement just enough code you do that first implement just enough code to get it to pass which could be like if the first test just asserted zero square root of zero zero then I would just return zero hard-coded that was the tester of a development idea and when I write the next test would have one assertion square root of what is one I might just return whatever you pass in right so far i've passed your test and the idea was i want to build up an interesting body of tests so my third test might be the square root of four is two well now i actually have to implement so that's kind of what you would do and now I have three good tests but what I think was important and useful about designed by contract that's lost with test-driven development is I don't have that specification I just have a like here's a few examples that I want to make sure work I mean I still have the the contract it's written in English but I don't have more of a formal way of writing the contract that you hadn't designed by contract so where you can get that back because like this guy doesn't say well 4 1 0 and 4 this should hold true right that's what we tested it says for any exits passed in right so you can get that back if you use a property based test a la quick check or Scala check and because that has a for all in it so it says for all X's of type double so long as and now we have to repeat ourselves which which is not a good thing I'm repeating the precondition in my test and in my require clause but if that pre condition holds then there's the post condition that's the same post condition we had before so using a property based test gets back that expressiveness of the design by contract and so what one of the talks I gave a few years ago was called the essence of testing and what I claimed was that this little statement of predicate logic is the essence of a test a little upside down a is for all and then X here will be of type double so for all X's P and Q are called predicates in predicate logic which are like you think of as functions that return boolean so if the P predicate holds on X in our case you could write P to be the precondition right there in Scala that implies the right arrows implies that Q would hold on the input and the result so f of XF is there our square root function f of X is the result of passing whatever X was to that and then my Q will operate on both of those so my Q takes both the X that was passed in the square root and the result it returned and it does its post condition right so that's what I think a test is is that it's a cus you can express a test as a statement of logic and it also is like a specification of the behavior of the function right ok so the other idea that I gave a couple years ago a talk called hope faith and proof and manera I talked about when to use assertions in production code and one of the things I think is useful is to use require clauses if it's a partial function square root really isn't defined on numbers less than 0 doubles less than 0 so you should say that at the top and blow up if right away instead of like letting that percolate through and you know that the the code doesn't know that there was a bug until some time later after they've already corrupted data in the database or something you want to fail fast but every time you user require I think it's good to think can I move that to the type so if I move it to the type like this let's say this is a double of it's positive zero and finite which means it's also not not a number so if I actually have a type then I don't need that require Clause right and what I what I want to point out about that is that that means that we have faith that types will implement their contract so like if you have a function that takes an int you don't do a require that the int that's passed in is greater than equal to int that max value and less than equal that int that I'm sorry greater than equal to n type min value and less than equal to m dot max value because we just assumed it will be even though we know sometimes there are bugs and sometimes types don't implement their contract the way we program is that's the thing we hang our faith on that's what we believe fulfills its contract okay so those are the two things that I want to start out with is just that you can specify a function and test it with property based tests with local statement of predicate logic of that shape and that we trust types implement their contracts in practice right okay so now what I want to do is is write a function to add two natural numbers and a natural number is 0 1 2 3 4 5 6 7 8 right so I can't really enumerate all the natural numbers because it goes up forever but what I can do is to find them inductively so what this is is two little rules that defines natural numbers and a little line the horizontal line it's kind of like if on top then on the bottom right so if and the the one on top there's nothing in the if so it's if true then zero is a natural number so I'm just kind of saying let there be zero zero is something I sort of just invent and say that it's a natural number and the bottom one says if P is a natural number that's the top line then the successor to P is a natural number so with just those two roles on day zero I can get a zero the next day I can get a 1 because P is zero and the successor to P is also a natural number now I have one and the next day after that I can get it to because you say well P is 1 so successor to P successor to 1 is a natural number I get two right so in Scala you can just write it this way and I'm gonna demo this so I have a sealed trait map and has a zero objects 0 subtype of Matt and it has a successor that's also an it you know subtype of an app those are the only two possibilities and successor takes a predecessor that's what the P is so I can just demo that guy so I can just say 0 that's a natural number I can say the successor to 0 0 this is arrow if I can type it so there's there's there's 1 and you can figure out what number it is by how many sucks it has in the in the in the expression so that's 0 that's 2 because I said suck twice so that's that's basically idea and I could I can keep going forever but you get the idea ok so far so good so that's a basic natural number data structure so now what I want to do is I want to make a plus method on it so I'm gonna add well I just did that so I'm going to add plus so to the Matt trade on top I just said the signature of my plus method is it takes another natural number and it returns a natural number right so that's an abstract method and then in the 0 I'm going to implement it by just returning the the right hand side so ah right it's just what I called the right hand side it's what you pass the plus essentially on 0 it just gives back the same thing I think that's the correct implementation and then in my successor case what I do is I say that I'm gonna claim that the successor to P plus some R is going to be the successor to P plus R so it's just one more than the addition of P plus R and what I did is I reduce the national number by 1 because P is 1 less than successor of P and then that would recurse all the way down to eventually you'll hit 0 which doesn't recurse anymore so that's the idea so let me just demo that grab that guy and after all this technology I'm gonna add very small numbers here's 0 0 so 1 is gonna be the successor to 0 right and 2 will make the successor to 1 and let's do it 3 oops - okay so I 1 2 3 0 1 2 3 so 0 plus 0 anyone anyone 0 so that worked you guys can go ahead and do these in your head you don't have to embarrass yourself to get them wrong right this is working I can say 2 plus 2 is 4 because you can count 4 sucks right 2 plus 3 so it looks like it's working now at least it works for 0 1 2 3 right but now what I want to do is Express something about the contract I'll just pick one thing which is addition is supposed to be associative so I go back here essentially I want to say this is I'm gonna advertise to you the users of my natural number library that Edition on natural numbers is associative and then I want to make sure it I'm gonna actually make sure that I fulfill that contract in my service to you as the library provider right so what that is is that if you add a plus B first and then add C for any 3 number natural numbers a B and C that's gonna equal adding B plus C first and then adding that to a right that's associative and so one thing I could do is is I could make test-driven development right I didn't do that but I could do test ii right test ii development and actually write a few examples so I have 1 plus 2 Plus 3 equals 1 plus 2 Plus 3 buddy actually do that see if it works because we have these 1 plus 2 Plus 3 equals is that how I did it I think I did it wrong whoo I did it wrong hang on a second let's do it right now I did this way doesn't matter either way 1 plus 2 Plus 3 it should be true okay so I did one example base test right um I could have one that adds up to 42 because I think that's important it's the most tested number and keep going but I can't of course test everything right and what I really want to say is that for any a B and C or for all a B and C this equality should hold that's what I want to say about my function and there's no this is the Q really it's the post condition it's not a precondition um there's no precondition any natural number will work so I can do that with the property based tests like that I just say for all natural numbers a B and C and then I have my associative equality check and we can try that because I have that happen it's kind of like a cooking show I have it already finished over here now we have to do is wait for IntelliJ to compile it ibly so this would be a good time for music okay that actually you can't see this teeny tiny little thing it does pass but I also inserted in my in this a little info so you can see what stride essentially I'm saying for all but I'm really just doing example based testing still so we're gonna run it out here so you can see the two strings just say test this is running the same test you can see that here I tried 31 34 62 13 76 63 you can see what those look like in you know in my memory and efficient natural number representation and the reason is if you look at my generator when you do property based testing you need a generator to generate the types of generating natural numbers by just taking inch between zero and 100 and trying those out so I never test anything above a hundred and I now test all combinations of zero 200 because it's just that's ridiculous it's too many right so it's still there could be some set of numbers even between 0 and 100 that don't pass this test and my my there's like a correspondence between the way we do software testing is a lot like science what science does is they scientists think of hypotheses like like I think this is how something works in the universe and then they don't just like publish hopefully they do experiments they come up with experiments and they test their hypothesis right and so we have the hypothesis that our code works like I have the hypothesis that my Plus method are natural numbers associative that's my hypothesis but I actually write a test to do it but what I called this maybe Einstein because he's often quoted I see him quoted saying this but I can't find evidence that he actually said it and I keep finding evidence people say well he never said that so maybe he said it but it's a good quote about science and what he said is that no amount of experimentation can ever prove him right but a single experiment can prove him wrong so relatively has passed a lot of tests right they've done all kinds of experiments over the decades and it's you know it works doesn't mean that tomorrow there's not gonna be some experiment that has oh actually in this situation it doesn't work and that kind of is what he did to Newton right for I don't know how long the Newton's law is kind of that people thought they worked because they were looking at larger things and when you get to smaller things you know they they don't necessarily hold or liro their speed of light things like that right so so the questions can we do better than Einstein as programmers and I think we can because our code is like math and what mathematicians do is they do proofs right I mean that's like that's that is math right one plus two plus three is associative so I could do a a proof by taking sort of by taking one of these sides and I start with that and getting and doing some transformations to it that are valid in my belief that they're valid and then I end up on the right hand side that proves that that one plus was a is 1 B is 2 and C is 3 that addition is associative for those guys so I'll start with a left-hand side and then one month I can take one into and say well that's the same thing as 3 and then I can say well 3 + 3 is 6 well 6 is 1 plus 5 right and 5 is the same thing as 2 plus 3 and therefore I proven in so I just that's a proof sort of how you do it but if only this is kind of like a unit proof I could do another unit proof for that other test case so I'm like just it is a proof but it's like not a proof that all a B and C you know that holds true right so I wanted to illustrate how did how one might do that it's not easy and this is probably like what are the easiest proofs we could come up with so it's very difficult to do proofs in practice about things but what I'm gonna do is I'm gonna try to approve that thing on top for all ABC my my implementation of natural number addition on my data type is associative that's what I want to prove so I'm gonna use the code so like if you look at the comment the the lower comments a 0 plus R equals R you can think of left side of that is if someone calls that at the client in the client code calling my line to my library into the plus method what I'm kind of gonna do is I'm gonna execute the right-hand side I'm just gonna return R so you could just replace that I mean if this code was in lined it would just replace your plus R with r right so that's an equality I can use and I actually want to use my implementation because I'm trying to prove my ability ssin meets its contract and then this one at the call site somebody has a successor which means there is a predecessor if you add R to that then you could replace that with the right hand side saying that if you add the previous natural number to R and take the successor that's gonna be the result so I can give him the shape on the left I could replace it with a shape on the right in my proof and vice versa right those are equal so so that's what I have and the other thing I'm gonna let myself do is add and remove parentheses but I'm just gonna say this is what I'm going for and I'm just gonna take these two equalities and try to prove you know with those two things the thing on top and so I I can't do it by an enumerated I mean I we've already done two of them you know one two and three past this and the other one I did was twelve seven and twenty three but there's just too many combinations right so I can do my proof inductively in the same kind of way we defined that natural number begin with I can say well I'm just gonna try to prove this zero case by heart hand Kota just like that kind of like I prove one two three I'll just prove that one and that that will be just sort of no precondition and then given a P some natural number P if it's associative with any B and C then I want to I want to prove that the successor to P is associative and so now that I have 0 I can plug in 0 for P and I've proved that one is associative if one is a if I have one I can now plug one in for P and now prove that two is associative and it goes on forever basically I've proved that my implementation it is associative okay that's one I try to do if you want to look at it as an algorithm because you you know we're programmers and we think you know like programming I would say if a is 0 then I need to prove the top one else it's definitely successor to P that's the only other case so I have a P and all we need to prove is if the P case is associative then its successors associative is associative and that will give me my proof okay so this one is pretty much similar to one two three I start with the left hand side right a is 0 and then I just say well I have that that rewrite rule essentially that 0 plus R is R so let me just get rid of the 0 there and I have B plus C I can take the prints away I can reprint the size that's allowed and then if you think of B plus C now as R on the right hand side I can go back left words and stick a zero plus in front that's allowed right that's that's just an IR I actually proved it so so that's my zero case that was pretty simple it's like just as easy as one two three actually that's the same technique right okay so now the more tricky one is successor so what I have here is I'm assuming I'm gonna assume the top part like I have to prove given the top part is true prove that the bottom is true right so I'm taking this as a given or the thing on tops like an axiom that's just believed to be true and now can I prove the other one right so so I'll start with the left hand side again where a is now successor of P and the first rewrite is the shape of the thing in the parentheses is well if it is that the the which one is it the shape of the guy in parens is the shape of the left hand side where P is y and b is r so I can rewrite it to the right right hand side just that the leftmost parens I'm rewriting from left to right off that rule so successor of P plus B is what I change so I just changed that one inside part I'm gets a little bit hard to follow but this is kind of illustrative of how these are tricky to do so now I just removed that one set of prints and I have this shape right and so now what I can do is I can go and re parenthesize because if you think of P plus B in this case is y then I can say well that's the success of me up did I say left or right I go left to right yeah so in the previous line y is P plus B and R is C so I can rewrite it the right hand way where the whole things imprints a successor of P plus P plus C right so now the problem is I'm a little bit stuck with my rewrite rules I can't really use one of them but what I can do is remember that I'm assuming that P is associative right so if you look inside inside the prince here and ignore this successor thing for a while I have P plus B in France plus C well that was if I go back to my little guy here P plus B plus C I could rewrite it to the right-hand side of the top line because I'm assuming that right I mean that's one way to look at it the other way to look at it is I'm actually recursing using the same proof so see how I just wrote it rewrote it to the right hand side that's my assumption or my axiom and now I just do one more rewrite and I've got my you know my proof so that's a proof that our implementation fulfills its contract of associativity and those are really hard to do but that's kind of the idea okay so so what my the the point of this talk that I wanted to get to is that I do like design by contracts formal specification of contracts with code but I didn't like that this these are things that can blow up at runtime right so if you actually are able in your language to attach the little statements of predicate logic to your functions into your classes to your bits of code then that is how you can specify the behavior in a more formal way I think that's a good thing and then you can you can reassure yourself that your your code is fulfilling its contract in two different ways one is you can you can write a property based test which is really like a fancy example based test but it's got a lot of nice properties so to speak but you can also use a proof in other words it's the same input so this is like a way to specify the behavior and then it's a starting point for either testing or proving and proofs are very hard to do a lot of the time so what I think a lot of dependently type languages they kind of try to prove everything and they turn off partial functions so that you can't use you know bottom the bottom type that sort of prove things that aren't true and I don't think that's necessary to get value out of it what I think that you can do is look at each proof individually and you just take the types that are involved in your function the things that are passed to you the things that you instantiate use internally the thing you return all those types you just assume you take it as an axiom that they fulfill their contract even if it's not been proven even it's just tested because that's actually what we do anyway so the function that you know takes a natural number and converts it to an int I would assume that right there that natural number fulfills its contract even if I haven't proven everything and I would assume that it fulfills its contract even if I haven't proven anything and if this code is simple enough maybe I can actually prove that code fulfills its contract so long as and it would be like the thing above the line is all the types that are involved fulfill their contract if that's true then then my method actually Falls it fills its contract so that's because in types types are the things that we trust you I said what's what we believe this is real I feel like I'm in church here but this is what we believe is actually true even though we know sometimes it isn't so that is my talk I just before I take a couple of questions our team a we do consulting so if you're interested in joining us we have talked to me if you have Scala issues you want to someone to help you with you can contact us mn I'm also on the Scala Center Advisory Board and I represent the community and people in this pilot community are not complainers in general so I actually find it hard sometimes to gather it's like pulling teeth like what's what do you what are your pain points so please feel free to come up and talk to me and complain to me or just tell you what your concerns are and I can take them back to the Scala Center so that's that's all I have so we'll get a couple minutes for questions if anybody has a question and I have a mic you suggested maybe we should go back and read Meyers Eiffel book and then now take that to heart no Meyers Eiffel book is quite large and it's got a lot of heat I think he fleshed out a lot of interesting things I went back and read it like all the stuff you wrote about various things but what I think he what I liked about design by contract was that it's a formal specification of the contract as opposed to what we use which is English this is like I go back that slide this is what's a little bit you know think wow it's way back here second slide I think that one I think there's something better we can do I think it should be on the outside but no language going to let you attach logic as a statement of contract at this point that I know of so there's one over there okay Shh I I don't know I think the people who design programming languages or tools that help us ensure code is correct could do this you could do this from the outside - like there's test frameworks that are external and there could be proof frameworks that are external that lets you do proofs but proofs are really hard so Mike my point was that by using a statement of logic you can easily use a test or a proof and then proofs don't have to really they can assume that everything is correct and then your proof is simpler it's more small so yes somebody had a question out there oh yeah so I think that jml allows you to do like first-order logic in Java is it possible to use it in Scala - to accomplish what oh great okay I'll try jml is Jamie let me do proofs where does he just let me know you're I don't know but yours you can write like for all statements in stuff like that I like okay I'll take a look at that okay jml anybody else yes are you yes that one yes right yeah that's a great comment I'll repeat it since we're on the mic is he just said did I not just essentially move the problem to the call sites now before the problem was in one place the potential now it's in a hundred different call sites and so what I talked about in the hope face and faith and proof talk that's a kind of long version the short one is that what I think often is a case at the call site is that you have nearby evidence so I called a require is an expression of hope as the designer of this function I hope no one ever passes a negative number but I don't know whereas at the call site usually it can be an expression of faith I have nearby evidence I did something I just squared it and so I have faith that that will always be positive right next to right before I call it or something like that so that that's the one of the points of that hopefully them proof talk was that another kind of assertion that I think is good is when you assert that it's positive there and move it to the type and now it's in the type because in types we trust right a lot of a lot of times like in the in the scholar book there's a there's a algorithm for doing quick sort where there's one function that takes a sorted list but it's not in the type so if we could you know assert there because I have evidence that I know it's not empty or there sort of because I just sorted it or whatever then then that's that's better I think it's better even though there's more places where it could possibly blow up at each of those places if there's evidence nearby that will always succeed then I think that's another kind of assertion that's a good to have in your production code because right away you move that thing you just proved with an assertion at runtime into the type okay yes oh sorry hi yeah I was just wondering if you had looked at the stainless project in a seamless I have I will look again I have looked at stainless I think yeah I don't I can't I don't want to say anything about it that might be incorrect to you do you know can you summarize what it is stainless without that mic you can give him like yeah just give it a summary so it's a project from the Lara lab at EPFL to sort of add a lot of the predicate logic based form over verification that resembles what you were describing okay let's do a subset of Scala great to a subset yeah it's a uses a subset of scotland tries to do that I have looked at that I have a question oh yes um it's actually interesting that you mentioned in the word Church which happens to be the last name of a famous mathematician yes this guy of Lombok a lambda calculus what about the fact that no axiomatic system is complete so basically there will be a bunch of true statements that will never be probable okay this is kind of a church the Church of Church exactly the Scala conference so what do you said is like no it's not complete I'm not sure how that affects proofs what what I have I would say that essentially I may not be too able to let me just go back the last slide I may not be able to prove everything and I think that's okay because we don't prove anything today I mean so if we can do a few more that are actually proven imagine if the standard library had a lot of proofs that might be useful but then then they find a faster way to do something where it's hard to prove and they reimplemented and they just test I think that's okay too so that that's not that's kind of a fuzzy answer but I just think it's it adds value even if we can't prove everything totally agree thank you yes apparently Scala 3 is gonna have spaces on dependent types I don't know if that's gonna be exposed but how does that affect the creation of types and so on yeah so dependent types is a way to do this it's I think if what a proof framework would look like for scholars be like a little differently type language that knows how to like do these kinds of rewrites these guys right here where are they yeah like the things here which you know you'd have to have inheritance and that kind of stuff and have to understand that the Currie Howard isomorphism I think it says two things to me one is that it there's something fundamental about this you know type theory that it was discovered and it came along and three different ways there's also a category three kind of branch of it that independently people came up with the exact same thing and it also is like for programmers is a great way to write to do proof so you don't have to do it on pencil and paper you can actually code this in a Agda or something or some proof framework or something and that's how we do it that you can express that thing in top as a type type of a valve and then if you can actually write a code that compiles you've actually proved that that for all statement and it's a really for programmers I think that's the way we would do it probably yeah all right that's time for questions thank you very much thank you so much I mean come on talk to me [Applause] [Music] [Applause]