Player is loading...
In Types We Trust
Bill Venners, Artima, Inc
Wednesday, June 12, 2019 · 10:15 a.m. · 44m 09s
Scala ensures that types are used consistently with their declaration, but checks only the name and structure of the types. A type also implies a semantic contract, which is typically expressed in human-language documentation and checked by tests. Can we do better? In this talk I will propose that we formalize the specification of semantic contracts as statements of predicate logic. I will show how these statements of logic can be used in both property-based unit tests and proofs. I will show you new features of ScalaTest that support this approach.
Embed
Transcriptions
Note: this content has been automatically generated.
00:00:00
oh you can i mean
00:00:01
good morning
00:00:04
good morning okay i just thought you say good morning back to me
00:00:10
um my name's bill banners and this talk is kind of about faith
00:00:14
a a a a a been a a thing about uh how
00:00:19
to make testing better for many years 'cause we do still test entertainment
00:00:23
and uh um that let me towards proofs and uh so
00:00:28
today uh i'd like to kind of build on a couple the talks that i gave in the last few years
00:00:33
so i'd like to start out by a kind of refreshing going back to couple things i i talked about in the past
00:00:38
uh two years ago it's holidays uh i had a talk called uh the essence
00:00:42
of testing and what i did in that hockey is is very short version of it
00:00:47
um i sure this lie this is a a a page of
00:00:50
eiffel code um it i for the language created by bertrand meyer
00:00:56
who uh was french still is french and he named his language after
00:01:00
the eiffel tower any an idea and they're called the design by contract
00:01:05
uh that was uh what he called this uh uh
00:01:08
idea of using assertions to specify the behaviour of functions
00:01:13
uh behaviour software so what i'm you do and i fall this this is the a square function in life or
00:01:20
as i can't just like to write square root implement the algorithm to
00:01:23
compute the square root i also have to specify behaviour of this uh
00:01:28
this function which we call the contract and it's kind like what the service provider promises
00:01:34
uh and what the person using it promises you gonna captures that insertions
00:01:39
so um there's three parts to a function in eiffel you have
00:01:42
the uh require clause which is what he called preconditions that's uh
00:01:46
basically had three kinds of assertions preconditions post conditions invariance so hear
00:01:50
what i'm saying is that a square is actually a partial function
00:01:54
because it's not the final negative real numbers just only defined on some of its input values not
00:02:00
all of them so uh what will happen is that if a a negative numbers past the square
00:02:06
root this will throw assertion error essentially at run time right um but what you're doing here is
00:02:12
also specifying that the client and this is the responsibility the client in the design by contract world view
00:02:19
the responsibility to pass in only positive or zero
00:02:23
positive reels are zero is the responsibility of the programmers were calling square root
00:02:28
right um and if they they'll do that that's a bargain there are punished
00:02:33
uh you are we are punished by getting an exception right assertion air
00:02:38
okay then do is where you do the algorithm like actually compute the square root
00:02:43
um ensure is called the post condition that's another assertion so what that is
00:02:49
capturing is what is the person who
00:02:51
implements this algorithm promising right so what uh
00:02:58
this one does is there's magically an eye full something called result
00:03:02
uh and that is the result it's about to be returned from
00:03:06
the squared function that was kept computed by the do part and uh so we square that in
00:03:12
basically this is was to be scared of x. right so if you square discrete of x. in the mathematical world it would just be x. you know
00:03:18
but in the world of fourteen point masses like float or double installer there may
00:03:23
be some rounding differences right so we do is we square the act was good result
00:03:28
that's about to be returned you subtract the original x. in in the ideal world that would be zero
00:03:32
right um but there may be plus or minus a little bit rounding difference
00:03:37
and so we take the absolute value that make sure it's a positive difference and
00:03:41
then just make sure it's below a certain tones were willing to except for routing
00:03:45
right and that's the post condition so one of the ideas that uh that he fleshed out in eiffel
00:03:51
is that assertions can be turned off at run time in production 'cause they actually take time to compute and
00:03:56
they're more about like making sure you got your code right uh so in develop and test of like if you
00:04:03
you don't have to ask you a department that's just responsible for testing in those scenarios you
00:04:07
would enable all the assertions and maybe checking all the time it might be a little slower
00:04:12
but when you play production my term is off and he had very fine green way of training things on and off
00:04:17
um you could turn on post conditions are preconditions invariance uh
00:04:22
separately and actually just turn them on and off for one particular function
00:04:25
if you want to an eiffel so that's that's what i was is idea
00:04:28
and this didn't really when in the marketplace of uh uh you know what happened was that uh i thought kind
00:04:34
of lost the c. plus plus it was competing with c. plus plus for bind a share and sort of lost
00:04:41
i'm in c. plus plus didn't have this and then java came along it also didn't have this and then uh
00:04:47
jen unit came along and test driven development and that really did succeed in the market place
00:04:51
so what we actually do on the g. the i'm not just in scholar but also but also
00:04:55
just generally on the j. v. m. is we do what's that of faults in an eye
00:05:00
for the fault and i feel is require run are turned on their enabled and ensure is disabled
00:05:06
right so we'll do in like if this is a square root function in uh
00:05:12
stall i would normally have a require clause to capture my preconditions and um
00:05:18
uh what this function does is if you you fascinated under matt
00:05:22
negative number to math that square root will give you not a number
00:05:26
so here it will instead give you an exception right so that's sort of the value added
00:05:30
in colour value getting exceptions another number uh over math a square root that's what we're doing
00:05:36
so we say require that the number passes not not a number it's
00:05:40
greater than it was zero and it's not positive infinity if that's all cool
00:05:44
then we can comment that's critters return result right and then
00:05:49
we don't check the most conditional yesterday martin showed ensuring in keynote
00:05:54
and ensuring is really so scholars the answer to ensure in eiffel seeking to design by contract install also
00:06:01
we show the inside the installer three with implicit functions like you can actually just a
00:06:04
result just like you couldn't like fall so anyway that's that's not common yeah some people
00:06:09
use that and i i was in the front row so either everybody behind me used in i just don't know i think most people don't use that right what we do
00:06:16
if we take that post addition we put that in this other place called the tests um
00:06:23
so ah test different about the blood test driven development was kind of like suggesting that you
00:06:30
write a test for so i might write this first assertion first square to zero should be zero
00:06:36
and then i go implement my screwed function just return zero and then my test passes then i'd another test another
00:06:42
assertion spirit of one should equal one now my test fails again so go actually implement my algorithm for square root right
00:06:50
and um uh what that doesn't do though is it doesn't capture the generality
00:06:57
of what bertrand meyer had in eiffel it if you look back here what he's
00:07:02
saying is really about all possible values of type real all inhabitants of type real
00:07:08
um for all reels you know if x. is greater than or equal to
00:07:13
zero then after you you know the answer you get that comes back from this
00:07:18
function should hope you know the post condition should be not be true about so this just says
00:07:24
well one zero and maybe forty two or whatever i think are useful things to try um uh
00:07:30
and this came to be called example based testing after property based testing
00:07:34
came along so what you can also do in in in a stall
00:07:37
is user probably based test where you get the sort of the same
00:07:40
generality that you get with like four with divide by contract from um
00:07:46
i can say for all doubles whenever and and i just repeat the preconditions i'm repeating
00:07:49
myself so i say don't require in the production code and i say it in the
00:07:56
whenever and the indices like skeletons of the
00:08:01
a property and then i compute i call square root and passing x. i get a result so
00:08:07
that's my result comes from and i do this sort of the posting doesn't check that's suppose condition check
00:08:12
a simple citizenship so that's actually what happens to design by contract if you
00:08:17
if you don't stick it in the code any actually move it out to the outside is you you you need a for all
00:08:23
and so that actually looks like predicate logic so the talk i would uh i get two years ago
00:08:27
the essence of testing i said well this is actually what a test is sort of the the the
00:08:33
by nature it's a statement of logic that in upside down a is for all so for all x.
00:08:39
p. i. n. q. r. predicates it this predicate logic you could have a predicate
00:08:44
function that takes input and returns boolean right um so p. i've actually kind of
00:08:49
said for for by square it function f. a square root that's the function i'm specifying
00:08:54
uh the type of x.'s double so for all x. actually means for all inhabitants
00:08:57
of double and then includes not a number 'cause that's an inhabitant of double um
00:09:02
so deaf p. double it takes a double returns pulling it just has that precondition it's
00:09:07
true or false right that's the preconditions so if that's true that little arrow there means implies
00:09:13
um and that means source if the right so if the predicate holds then
00:09:17
people's condition should hold it the precondition is true then the prosecution must be true
00:09:22
i'm in the position is a predicate function that uh works off of the input like x. and the result
00:09:29
f. f. x. m. so in our case i'm gonna pass in the the x. m. as a result and i do my post
00:09:36
condition that's the same pose condition a math so that's that was
00:09:40
the essence of testing is that that uh you you could specify
00:09:45
they function on the outside with a statement of logic when
00:09:49
you specify on the inside it looks like design by contract
00:09:52
okay so that was that talk and then a year ago or two two years ago i give
00:09:56
a talk all hope faith improve uh which is mostly about where to use assertions in production code
00:10:03
yeah one of the places i suggested that we should we we do users
00:10:06
and it and then it makes sense is required clauses which are precondition checks
00:10:10
and the reason is that if something really is parcels where
00:10:13
it's a partial function we want actually capture that early so
00:10:18
i mean one thing user porpoises is it makes it really obvious that this is
00:10:22
a pretty little but this has this precondition it kinda says every clearly my code
00:10:27
but also run time you don't ever want that actually happened production but it
00:10:30
does want to happen as soon as possible so that you can detect it
00:10:33
so you don't wanna like just not check it and then go much farther
00:10:37
and save some crab data database before you notice there's a problem right um
00:10:42
so anyway what the what the what are the other idea that i i
00:10:48
i kind of had a net talk was that if you have a require
00:10:52
it's good to do them if you have a partial function that every time to do them you should think well can i get rid of this by moving into the type
00:10:58
so actually the type that promised it's not an odd number it's greater than zero and it's
00:11:02
not positive energy then i could get rid of the require cause so that looks like this
00:11:06
so actually i could go to the shelf and pull off a positive or zero finite double type
00:11:11
um then i could get the require cause and what i did is i remove one place that
00:11:16
uh this cable open production i call this an expression of hope because i hope no one ever passes
00:11:23
but you know a negative three to this but i have no evidence that they want right
00:11:28
i'm gonna do this the problem with that is that just move the problem to the call size
00:11:33
because if something was to call square root and they have a double in handicapped convert to this thing
00:11:39
and that could involve blowing up an exception right if it's negative but what i'm i think is
00:11:46
well usually the case of the cost side is you have nearby evidence that it will always succeed
00:11:52
so the other kind of assertion that i suggested it's good to use in production code is the kind where you
00:11:57
make an assertion with nearby yeah but is that it will always succeed if you believe you always exceed any movie to type
00:12:05
so this would like move this knowledge that uh you know this
00:12:09
is true about this value to the type of button caption type
00:12:13
and then i never have to check it again and what that
00:12:15
illustrates is that we trust types to fulfil the contract so just
00:12:22
if you pass me in and i never really you know do an assertion is the value
00:12:26
greater than or equal to men and unless anyone to max and i just trust that right
00:12:32
because i didn't trust typed implement their contractor to fulfil their promises i have
00:12:36
put all kinds assertions all over the place so that's where we hang our
00:12:40
our belief on we believe that types gonna fulfil the contract we pretend even though we know there there are
00:12:46
bugs out there and sometimes they will fulfil the context people we we program is that we trust them okay
00:12:51
so that's ah since eighty two things from from past thoughts that went to cut every
00:12:57
start with a 'cause this talk build on top of the um the first one is that's sort of the nature of
00:13:02
how you would specify function f. of x. is a little statement of predicate logic and then
00:13:07
um we trust types to correctly implement the contracts impact is when we program when you write code
00:13:13
okay so now the new stuff um for this i'm gonna use natural number as an example
00:13:18
and uh what um this is also come like if and the top if it thing on
00:13:25
top of the line is true than the thing on the bottom of the line is true
00:13:29
so what i'm natural number is is uh well and computer science we just i was zero zero
00:13:34
one two three four five six seven dot dot dot right so it's actually an infinite set of
00:13:40
of our numbers ignorance right so what this is is a
00:13:44
way to this is using interruption to define an infinite set
00:13:49
with very finite set of rules right so the first rule is the base case and that is sort of like
00:13:55
we don't have any precondition that has to be true before on top there's nothing up there so that's gonna like true um so
00:14:02
there's just a zero was gonna clear zeros a natural number that's gonna like let there be zero
00:14:08
um and then the second rule he was inducted rule which says
00:14:13
if he is a natural number than the successor the p. is
00:14:15
a natural number like p. because that sensor predecessor um so uh
00:14:22
you know on the zero with they when you wake up um you can get zero because
00:14:29
it just that's free ages zero exists right let there be zero on day one the next day
00:14:35
i can say well seems imaginable there for the successor to zeros announcer
00:14:39
number and i get one right ninety two i can't get zero and one
00:14:44
so i can say well what is the national weather for the six axle one is a natural number and that's too right so
00:14:48
that was that sort of is how you define with induction an infinite i'm not the type and install you get it this way
00:14:56
um i say still trade met okay subjects you're extends net and
00:15:01
a case classic the stock um it takes a predicate uprights are a predecessor uh
00:15:08
which is a natural number right p. is the subject of net um
00:15:12
and that's my two cases and i can just dental that real quick uh
00:15:20
yeah i think over this guy um just the set in
00:15:24
their uh aspects it down zero with the little the a zero
00:15:29
well one so this is now have zero i can use the other ruled inductor rule and say
00:15:34
uh one is the successor to zero i can see to is the successor to one right
00:15:40
and then i could i could keep going but only have forty minutes for this talk um
00:15:45
but it it goes forever right uh so what you'll see here i i you know the way
00:15:50
i wrote this you get it does capture in the type what the number is to um and
00:15:55
in the two string you can see the nesting of these stock classes um and you can just count them so you know this is one because
00:16:02
it has won a stock constructor invitation there's two sucks here and that's um
00:16:07
to write and they're zero six years at zero okay so that's that guy
00:16:13
um and then now i wanna add a method to it a two
00:16:19
i mean at at uh to add to natural numbers um so i define a just a
00:16:25
a an abstract method um i still trait that that is plastics annette returns in that and um
00:16:32
then in my zero o. k.'s i just returned the right hand side
00:16:36
so it takes like all that are 'cause that's the right hand side
00:16:39
and you're adding zero to ending thing to zero is that whatever you added to zero
00:16:43
so that's that's that one and then over in the successor case
00:16:47
um what i do is basically the call so you have successor p.
00:16:52
plus one so let's say a up he is um three
00:16:57
plus one so the successor the three is for was one is five right so
00:17:03
what i what i do here they say well if you just add four plus one
00:17:07
but most say this is just a three piece three three plus one like it before and i think this is so
00:17:11
that they could be five that's the same thing and i'm what i'm doing is i'm calling myself aggressively with one less
00:17:18
uh then this uh so will eventually get the zero case which doesn't records anymore um second demo that i'd
00:17:25
just so you believe that actually does a uh huh
00:17:32
some have to my
00:17:35
my little uh
00:17:38
inventing
00:17:40
i could not try to talk on doing this equals equals success or of two for a one
00:17:48
that would look forever and then i'll just make three for the heck of it three equal successor to so you get the idea
00:17:53
so i say for example zero plus one um i get one
00:17:58
there's one stuck there zero plus three i actually get three stocks
00:18:02
uh_huh yep that's three if it's a two plus
00:18:04
three i should get five some encounters one two groups
00:18:10
three four five right so that's addition to okay so um
00:18:18
open it up that was edition and um now what i what i just read it has i don't know how to test first um
00:18:25
so i wanna read it a second uh and i wanna say that my a
00:18:28
plus method is going to promise that it will be associated right so um when i
00:18:36
i say basically a positive i've three natural numbers a. b. and
00:18:39
c. a. plus b. plus c. people's eight plus people see right
00:18:44
um so i could do a few example based test like this one plus one plus two plus three
00:18:50
must equal one plus two plus three right and then i have another one and so right so that's
00:18:55
example based test but you can also do the for all the thing i mean essentially it doesn't capture
00:19:00
this notion of that it's for all natural numbers a. b. c. um
00:19:05
i want this to be associated so i could go for all like this you
00:19:10
say for all natural numbers avian see i'm a plus b. plus c. must equal
00:19:15
eighty plus people see if it's kinda hard to say but uh so i'll say that that's i got that over
00:19:21
here um so so here's mine a natural number that's just like i had on the slide there um and then
00:19:29
in this is to use a property based test the one other thing i need is i need a generator for national numbers
00:19:36
and so here i just used to get him generator instead from zero one hundred because these things actually do take up memory of probably
00:19:42
in production would use a larger one but you wanna i don't wanna have it like zero billion because you might run out of memory
00:19:48
um so to say zero hundred and i just have a two net method it's
00:19:51
recursive lee you know takes a an inch and turns it into an actual number
00:19:55
um and then i'm done here i just say for all natural numbers a. b. and c. uh in as my little uh uh
00:20:04
assertion um so i can actually does it if you're
00:20:08
just from the test and you will see the passes right
00:20:13
so what i'd also wrote you're just gonna get let you see what uh
00:20:17
what's going on is our little function call to and that um
00:20:24
but inside here too and we'll take a natural number and return it because the the other direction
00:20:29
as model to net up here and it's again it's really cool records of a tail recursive loop
00:20:35
and so what made you now's for each one of these
00:20:38
uh test that we testament pronounce you can see what's printing
00:20:41
so you see the image or version of it and then you'll see the the actual natural number version of it here
00:20:46
um sort however much as you'll see a bunch of uh you know print
00:20:49
statements and then this this notice generator that'll be out in three that one and
00:20:54
we do twenty percent edge cases combinations like is one hundred
00:20:57
one hundred one um so little uh there's like a a
00:21:02
what's the next one one zero a hundred so here's one year zero and this
00:21:07
is what a hundred looks like an it things hundred as as case 'cause i
00:21:09
use it into between zero and a hundred and then we just kind of randomly
00:21:12
all over the place uh try stuff one of things i didn't try is hundred one
00:21:18
right because i'm only going zero hundred so even though
00:21:21
this looks like um predicate logic this for all um
00:21:27
it actually uh doesn't and it's still example based testing in
00:21:32
a sense 'cause i'm just trying different things so what um
00:21:38
i
00:21:40
what did i i had this light also in my hope face and prove talk and it's
00:21:44
called maybe i sent 'cause i says often quoted as saying this but there was actually no
00:21:50
evidence after the fact that he said it so maybe he didn't say that what what the quote
00:21:54
is is that no man of experimentation can ever prove me right a single experiment can prove me wrong
00:22:00
and so like the theory of relativity because it's it's like the theory to mathematical model
00:22:04
of reality um so the scientific method says we don't just take them and fey if we
00:22:10
try to do experiments to see if it you know actually holds and
00:22:16
no matter how many those experiments you do a that's not a proof
00:22:21
that it's correct some day like tomorrow there could be a experiment that
00:22:26
actually shows there's a problem with it and it needs to be updated right
00:22:29
so that's kind of what we do with softer development today when we write tests
00:22:34
is we're we're doing science we're we're saying well i'm not gonna have faith that my thing works even though
00:22:39
you know i make them think it's the it looks like it should work um i'm gonna test it
00:22:44
and make sure right and uh those tasks even if it's a for all because we're just trying certain
00:22:51
certain values uh doesn't prove that it works right it just uh
00:22:58
makes me more confident that it works um but if you have a
00:23:02
test that fails that's pretty close to approve that there's a problem um
00:23:07
either there's a bug in my algorithm or there's a bug in my test so there's a misunderstanding so there's a bug in our our communication or
00:23:14
there could be a bargain hardware who knows but there's a problem um okay so what um you can do him
00:23:20
in in programming is you actually can do better because programming at
00:23:24
least the functional part of your code is like kind of can
00:23:28
be treated mathematically and then you can do proofs so what i'm gonna do is i'm gonna prove one plus two
00:23:35
one plus two plus three equals one plus two plus three right um um
00:23:39
so what i'll do is i'll start with the left hand side of that equality
00:23:42
um and then i can say well one post these three
00:23:46
uh three perseus sex uh well sixes one plus five right
00:23:50
and five is too busy and for i did is i started on the left hand
00:23:54
side and i ended up on the right hand side so that that's my proof so
00:23:59
in when you see a mathematicians improve so you're in it with the q. e. d. or this'll square which is pronounced one ah
00:24:05
it means here's my proof right so i just did it um so i could do
00:24:10
that again with with this other example but it has been like example piece proof right
00:24:14
um what i haven't done is i haven't said that have proven that for
00:24:18
all natural numbers a. b. and c. associate of you know additions assertive right so
00:24:26
to do that um i wasn't actually do now and what i'm gonna do is a
00:24:32
multiple some sort of mathematical equality is out of my code so for the zero case
00:24:39
um what i can say is is your plus articles are because if the client a zero plus all our
00:24:45
what excuses it returns are so you you can can like see the left side
00:24:49
people side it sign is the client code the rights of equal sign is the body
00:24:54
right and then for the successor case uh the left side of the equal sign here is for
00:25:00
the client could again successor p. plus are that will invoke this function and that kind of substitutes the
00:25:07
the right hand side expressions which is the barking right successor of people's part are
00:25:12
in parentheses so now i i basically wanna prove uh you know my for all
00:25:17
probably b. c. uh addition is associated um from natural numbers
00:25:22
and i know these things and i also morgan allow myself to add or remove parentheses okay so um
00:25:30
because uh i mean one way to do this is just enumerate them right i say one plus two plus three equals one plus
00:25:37
two plus three i just do that so i could say well one plus two plus four equals one plus two plus four right
00:25:42
um but course again it's infinite so that you can never enumerate all of them so we have proof
00:25:48
by induction i um which premieres the where to find be uh
00:25:55
the data type in the first place so i'm going to proves it
00:25:59
does you basically i'm a substitute they for either zero or successor of p.
00:26:05
so in the zero case i'm gonna i basically a place people see become zero plus people see
00:26:10
and that equals zero plus and then per inference people see and
00:26:15
that one i'm just going to prove like i did one two three
00:26:18
right just to prove it right out right um but then the rest of it i'll use an adaptive
00:26:24
kind of proof right i say well yes p. plus b. plus c. equals
00:26:32
p. plus b. plus c. like that that's my like precondition if that's true then
00:26:37
successor fee plus b. and friends plus e. equals success
00:26:41
or the plus people see and that that's sort of my
00:26:45
you know i have to prove that info and what my my my uh
00:26:48
you know claim is is that if i prove both of these then um
00:26:53
that proves that my addition is associate magician method okay so um
00:27:00
because we're programmers yeah well 'cause i'm a programmer i think of this as a algorithm
00:27:05
so like given in a if a is a zero like you know you could say a match case zero right
00:27:12
if it is zero then i needed prove this for all
00:27:16
b. c. zero plus b. plus c. balls zero plus people see
00:27:22
otherwise yesterday isn't zero that means it has to be a successor and there's a p. m. or so
00:27:28
i was need to prove for all p. b. c. and there's my if
00:27:31
that right there's like the top and the bottom of that rule uh you have
00:27:38
people's be in france plus equals p. plus b. plus c. right
00:27:41
if that's true then i need to prove this this bottom line right
00:27:47
okay so that's algorithm so listed the zero case first um um
00:27:52
so i'm gonna start with the left hand size basically a a zero now and so that means
00:27:57
that the you know the left hand side of my uh equation is zero plus b. in principle see
00:28:02
so what i can the first re right i can do is because i know zero plus articles are i think it really does your plus there
00:28:10
in other words i have one of these you know equations you oppose
00:28:13
articles are that's actually from my code them trying to prove is correct
00:28:18
uh so um so i can use it to do a substitution and i can get rid of the parentheses
00:28:23
because i'm allowed to do that and i can actually add a different set apprentice 'cause i'm uh do that right
00:28:29
um and now i can go back to my my rule go from right to left
00:28:33
so b. plus c. in parentheses you can see as or on the right hand side
00:28:38
so i can stick to zero plus in front of it right um and now i basically ended up
00:28:43
with the right hand side of my qualities it just i'm like away prove one two three i got
00:28:48
i got to uh be say just prove that base case um so um that's that one
00:28:56
and so now the the more tricky one is this guy um so i'm gonna start of the left hand side again and
00:29:04
it's ah essentially times over here i substituted zero for a
00:29:11
at the top line there are zero plus b. plus c.
00:29:14
that's one case the other cases i'm searching successor p. for a
00:29:18
so that's why start with that so successor people's be in prince plus
00:29:23
c. that's we start with so now what i can do it is
00:29:26
inside the trends there i have fish the left hand side uh like
00:29:31
at the shake successor y. plus or except you know why is key in
00:29:35
r. s. b. so i can actually change it to the right hand side
00:29:39
so now inside the the other friends there it's it's successor p. plus p.
00:29:43
that was that's actually from my code that's why codes gonna do um and then uh
00:29:50
i can get rid of those extra friends that they don't maybe
00:29:54
more for that that same rule being able to add and remove courtesies
00:29:59
and then use this rule again it's the same like the look it is
00:30:01
has that left hand shape again uh where y. is no p. plus b.
00:30:06
and our is c. so i can make it look like the right hand side again this is like referring
00:30:10
to my codes like i was gonna do um the successor of now i have successor people's b. plus c. so
00:30:18
we now i'm stuck so i maybe something kind if he uh
00:30:26
here and i'm actually gonna call the proof that i'm using i'm
00:30:30
gonna actually use the proof that i'm haven't finished yet in the uh hope that i will be able to finish it so what
00:30:37
if you look at the inside of the prince's so says success or per ends to look what's inside
00:30:42
there it's in friends people's be been plus c. right if you look up on top that's the shape
00:30:49
of the left hand side but that's that's actually shape uh let inside um and
00:30:55
also the shape of like if you look at the first line their successor people's b.
00:30:59
plus e. right it's the same shape so this proof one
00:31:03
printer prove is this is associated and if i actually succeed
00:31:07
then i'll be able to actually change that that that that's what i'm trying to prove so
00:31:10
actually gonna be cursed call disprove recursive really if you think of it as an algorithm and uh
00:31:17
but i'm gonna replace successor p. by keys if you look at the first line
00:31:22
it says success or p. plus p. in france plus c. you know here that the second the
00:31:27
bottom line it says he plus people seasick it's actually one smaller and so the reason i can
00:31:33
i believe i can do this is because i went one smaller any even if i start at a at a you know a quinn till you in
00:31:41
eventually like this will re curse and get all the way to zero which doesn't records right
00:31:46
so anyway as long as we will finish my proof they should be okay um
00:31:51
and now uh the last thing i need to do is just one more step
00:31:55
though is i can do one of these rewrite again so this one is um
00:32:01
basically the the second the last line is back up on this line looks like the right hand side now
00:32:09
uh so what i can do is i can pull the successor out and so it's successor p. l.
00:32:13
plus b. plus b. and that's actually what i was trying to get that that then that proves the
00:32:19
the uh successes so that's sort of like the feel of how you do proofs and and what i did is i took
00:32:25
i sort of took my code and pulled out into somebody's little
00:32:28
mathematical statements and then i could do approve with that okay um
00:32:34
and it's hard so well there's been a lot of research in in in in recent years
00:32:39
about in the functional programming world about doing proves at like the penalty tight using it openly
00:32:43
type language so what i wanna show you is what this looks like in our dog is
00:32:47
a dependent fully depend only type language um which means you can the terms can show up in
00:32:54
types you can index the type by a term and so what i would have
00:32:59
to do to do this proven on this sort of like emulate mice colour code
00:33:03
um so i've got a a and eighty there that's sort of has the same shape as
00:33:09
my a natural number um i didn't show the vision method um
00:33:15
but what i have done here the bottom is like you could think of as sagas of al and hold on
00:33:22
and then to the right of that is it's type um and it's a function type the arrow there is a like a function arrow
00:33:29
so so like a val that refers to a function and it takes three natural numbers for all those can like syntax checker
00:33:35
um it takes through natural numbers and what it produces is it is and it ends it
00:33:44
a a plus b. in france plus c. will always be equal
00:33:49
to a plus b. plus imprint so this doesn't compute it computes
00:33:56
something of that type and so the what what what these
00:34:01
uh depend only type languages like interests and and on the
00:34:04
do is they use the curry howard isomorphism to say that uh propositions are
00:34:09
the same thing as types like berkeley correspond to types and programs correspond approves so
00:34:15
if you actually can you know you can describe a proposition unit type
00:34:21
i mean if you could actually get your program become pilot get inhabitant like for it actually implement that
00:34:26
you know make an initialise that uh about the value of that type that actually is a proof that
00:34:31
that proposition is true so that looks like this this is actually the same algorithm i just went through one
00:34:36
well not a paper but on slides um this is how you would do it and i'll get this came from phil what about bill waller has a uh
00:34:44
programming language foundations inaudible oak so he
00:34:49
this came from there um this our lock uh so you can actually do it mechanically a uh
00:34:55
and it's like programming so instead of writing tests which is like programming
00:35:00
you would write true switches like programming sometimes okay so anyway that's uh
00:35:08
that's what i like the looks like it's all the you know in the description of this talk i talked about like
00:35:13
using statements of predicate logic to define contract so so going
00:35:16
back to bertrand meyer he said let's define contracts formally with assertions
00:35:21
then what i'm suggesting i kind of wanted to like proposes as an idea and actually i'll be here
00:35:26
the nice thing about having my talked the first is you guys can come up and talk to mentally which i think it was very curious what you
00:35:32
think of this idea that we would as programmers actually did kind of the
00:35:36
the more formal specification of the contract that would not be assertions would be
00:35:41
statements of logic uh so like i might say for my class method on net
00:35:45
um superstars are are plus zero is our um that's like left identity right identity um this is
00:35:52
like the body of my my successor method i could say that i i that's annoys me true um
00:35:58
and then then i have a perl a. b. c. a. plus b. plus c. equals
00:36:04
eight plus people see that's associated of um don't have cumulative i may have other things right
00:36:09
and that's my more formal specification of the contract usually the what
00:36:13
we do on the g. java platform is we write it in english
00:36:16
um for the most part we say what this thing does um because if you do this then uh
00:36:25
you can either use property based test were proves to sort of give your self confidence that you are
00:36:32
meeting your promise and um essentially i'm promising all those things as the implement of nat
00:36:38
uh and i can just proves a really hard so maybe i don't have
00:36:43
time or a a or whatever uh so i can use a test um
00:36:49
and i think that's fine because because we have faith in types right but this would allow us to sort of gives an extra tool
00:36:55
like if we add like a a in addition to test framework utilise proof framework that sometimes you could use where was were
00:37:02
made sense then you'd have actually be better than testing it
00:37:05
would be better than science rate would be mathematical proofs so um
00:37:11
so anyway uh the uh that the other idea that i wanted to
00:37:19
sort of throw out there is the because we trust types um
00:37:25
we should be able to use the contract which is like these
00:37:30
statements of logic of any of the involves types that we use
00:37:34
as axioms so if we don't have to be just trust that they are they are fulfilling the contract whether
00:37:39
they had troops or not you know if they have if they just tested i mean i don't think there isn't
00:37:44
there's i don't know that there's any truce for and on the g. d. and that fulfils
00:37:47
its contract but i trust that it's going to be between you know been into max and
00:37:53
um and that's fine but you know that so i can actually use the uh like
00:37:57
i for my two at method that i showed you that sort of the the the
00:38:01
output in the test um one of the things that that that would have to do is
00:38:07
it's only this is a partial function because it's not gonna work for any integrated into well greater than um accent
00:38:15
so that would be my precondition for this like the p. x. um and then i have to somehow express uh
00:38:22
that you know if you count the the nested levels or something
00:38:26
then you get um the output right in that and approve of that
00:38:33
i could use all these all these guys for example because i
00:38:37
trust net to fulfil its contract i've been i would not actually
00:38:40
use the code even though like here the likes sort of this was based on the code i could re factor that code and
00:38:47
i need to make sure that still says is true even if
00:38:49
i'm using more efficient algorithm them then a successor people's or something um
00:38:56
you know i need to be i i like the other proves need to depend on the interface not the implementation of the code
00:39:02
um so anyway that's that's that's the idea so um
00:39:08
and and and the uh uh i kind of what i was thinking that like unit testing it has just look at one thing
00:39:14
so you you know proves not front with everything works much prove net and and work
00:39:19
just to prove my two and works i just assume all that other stuff works i take that as
00:39:23
an axiom and then then then then really what might prove says is the so long as net and and
00:39:27
fulfil their contract into and you know i've proven that it fulfils its contract so that's like all the unit proof
00:39:33
so anyway um that is my talk so before i go to questions i
00:39:36
uh just wanna mention that we do uh we are hiring actually we do consulting
00:39:40
um we are available if you need help and then i'm also a member of the advisory board
00:39:45
well this colour centre so i actually represent the community um so if you have any
00:39:49
concern please uh come up to me at the conference uh look like this and uh
00:39:54
i also these brown bag so uh if your company would like me to come in like
00:39:58
over i mean uh probably over video or whatever um it's kind like the psychiatry session uh
00:40:03
you get on the couch and i show you ink blots yeah i say this you know this is colour what you see
00:40:09
and you tell me like what your concerns are what you like which don't like um i can kind of
00:40:13
bring that back to sell centre so anyway um are there any questions you have like a few minutes for questions
00:40:22
yeah
00:40:26
yeah it's gonna bring around uh the microphone if somebody has a question thinking well i'm we welcome where you with a high it's
00:40:36
that's what that that i'll constant well i think it's it's
00:40:40
not really fall long because can get is online it's it's
00:40:46
how d. nonstop um oh uh well uh i think what you're saying
00:40:54
is that uh if i do this proof here for example this guy um
00:41:01
it's not even ever go back to this as a collective this guy um if i prove this it actually
00:41:10
i think it's okay because what you're saying is computers actually can't get up to open trillion 'cause will fit in memory um
00:41:17
but all the ones we can get to our
00:41:22
i would i would i've proven that is correct all the ones the
00:41:25
computer could actually fit fit in memory um and that's better than testing
00:41:31
is my point so i i think uh
00:41:35
you know that is like proof in the mathematical senses and crew for like especially you know prove it's not proof
00:41:41
absolute prove beyond always have to prove beyond any doubt it
00:41:45
isn't um but it's so useful uh it's like um if
00:41:52
you know it's kind of like an axiom if everything fits in memory and you know natural number and and fulfil the contract in
00:41:57
my two and met and this guy fulfils its contract that's all improving it's like a unit proof and that's good enough i think that's
00:42:06
yeah anybody have another question
00:42:08
people spread out way back in the back yes
00:42:12
um
00:42:22
i thank you for your cock was great thank you um
00:42:28
most of those solutions to that one improves by march some yeah
00:42:33
and the mouse there are different box grooves raw bar come production more yeah
00:42:39
otherwise have you can remember i'll uh
00:42:43
yeah i mean if you look up uh so spruce fir associate as
00:42:46
much of ways to do it um so what i wanted to do was
00:42:51
you will be similar to programming right so when you twenty typically type language you think of like are the
00:42:56
as a proof framework for scholar that you have to it's not very
00:43:00
integrated um and that's one of the things audit does is that kind of
00:43:04
a recursive recursion for um but yeah i i don't i this is as far as i
00:43:10
got is is just so that kind of figuring out that that this is sort of like
00:43:19
i think they just make sense it i just letting it be nice
00:43:21
to have a more formal specification of contracts and end up looking like logic
00:43:27
uh which is perfectly match you know probably based has looked exactly like that but sort of proof so that that's uh
00:43:35
you know how to how to actually do proves is is it is uh i don't know i haven't done too much with that
00:43:40
um and i just think what i would have observed is it's really hard to do proofs
00:43:45
i think kind of find it's like solving puzzles but it's not like you know you can write test but you can't necessarily do approve so
00:43:53
anybody else
00:43:56
millions
00:43:59
and once i i mean i mean thingy in okay cool well thank you
Conference Program
A Tour of Scala 3
Martin Odersky, Professor EPFL, Co-founder Lightbend
June 11, 2019 · 5:15 p.m.
8337 views
A story of unification: from Apache Spark to MLflow
Reynold Xin, Databricks
June 12, 2019 · 9:15 a.m.
1267 views
In Types We Trust
Bill Venners, Artima, Inc
June 12, 2019 · 10:15 a.m.
1569 views
Creating Native iOS and Android Apps in Scala without tears
Zahari Dichev, Bullet.io
June 12, 2019 · 10:16 a.m.
2231 views
Techniques for Teaching Scala
Noel Welsh, Inner Product and Underscore
June 12, 2019 · 10:17 a.m.
1295 views
Future-proofing Scala: the TASTY intermediate representation
Guillaume Martres, student at EPFL
June 12, 2019 · 10:18 a.m.
1156 views
Metals: rich code editing for Scala in VS Code, Vim, Emacs and beyond
Ólafur Páll Geirsson, Scala Center
June 12, 2019 · 11:15 a.m.
4695 views
Akka Streams to the Extreme
Heiko Seeberger, independent consultant
June 12, 2019 · 11:16 a.m.
1552 views
Scala First: Lessons from 3 student generations
Bjorn Regnell, Lund Univ., Sweden.
June 12, 2019 · 11:17 a.m.
577 views
Cellular Automata: How to become an artist with a few lines
Maciej Gorywoda, Wire, Berlin
June 12, 2019 · 11:18 a.m.
386 views
Why Netflix ❤'s Scala for Machine Learning
Jeremy Smith & Aish, Netflix
June 12, 2019 · 12:15 p.m.
5026 views
Massively Parallel Distributed Scala Compilation... And You!
Stu Hood, Twitter
June 12, 2019 · 12:16 p.m.
958 views
Polymorphism in Scala
Petra Bierleutgeb
June 12, 2019 · 12:17 p.m.
1113 views
sbt core concepts
Eugene Yokota, Scala Team at Lightbend
June 12, 2019 · 12:18 p.m.
1655 views
Double your performance: Scala's missing optimizing compiler
Li Haoyi, author Ammonite, Mill, FastParse, uPickle, and many more.
June 12, 2019 · 2:30 p.m.
837 views
Making Our Future Better
Viktor Klang, Lightbend
June 12, 2019 · 2:31 p.m.
1682 views
Testing in the postapocalyptic future
Daniel Westheide, INNOQ
June 12, 2019 · 2:32 p.m.
498 views
Context Buddy: the tool that knows your code better than you
Krzysztof Romanowski, sphere.it conference
June 12, 2019 · 2:33 p.m.
393 views
The Shape(less) of Type Class Derivation in Scala 3
Miles Sabin, Underscore Consulting
June 12, 2019 · 3:30 p.m.
2321 views
Refactor all the things!
Daniela Sfregola, organizer of the London Scala User Group meetup
June 12, 2019 · 3:31 p.m.
514 views
Integrating Developer Experiences - Build Server Protocol
Justin Kaeser, IntelliJ Scala
June 12, 2019 · 3:32 p.m.
551 views
Managing an Akka Cluster on Kubernetes
Markus Jura, MOIA
June 12, 2019 · 3:33 p.m.
735 views
Serverless Scala - Functions as SuperDuperMicroServices
Josh Suereth, Donna Malayeri & James Ward, Author of Scala In Depth; Google ; Google
June 12, 2019 · 4:45 p.m.
936 views
How are we going to migrate to Scala 3.0, aka Dotty?
Lukas Rytz, Lightbend
June 12, 2019 · 4:46 p.m.
709 views
Concurrent programming in 2019: Akka, Monix or ZIO?
Adam Warski, co-founders of SoftwareMill
June 12, 2019 · 4:47 p.m.
1974 views
ScalaJS and Typescript: an unlikely romance
Jeremy Hughes, Lightbend
June 12, 2019 · 4:48 p.m.
1377 views
Pure Functional Database Programming‚ without JDBC
Rob Norris
June 12, 2019 · 5:45 p.m.
6374 views
Why you need to be reviewing open source code
Gris Cuevas Zambrano & Holden Karau, Google Cloud;
June 12, 2019 · 5:46 p.m.
484 views
Develop seamless web services with Mu
Oli Makhasoeva, 47 Degrees
June 12, 2019 · 5:47 p.m.
785 views
Implementing the Scala 2.13 collections
Stefan Zeiger, Lightbend
June 12, 2019 · 5:48 p.m.
810 views
Introduction to day 2
June 13, 2019 · 9:10 a.m.
250 views
Sustaining open source digital infrastructure
Bogdan Vasilescu, Assistant Professor at Carnegie Mellon University's School of Computer Science, USA
June 13, 2019 · 9:16 a.m.
374 views
Building a Better Scala Community
Kelley Robinson, Developer Evangelist at Twilio
June 13, 2019 · 10:15 a.m.
245 views
Run Scala Faster with GraalVM on any Platform
Vojin Jovanovic, Oracle
June 13, 2019 · 10:16 a.m.
1340 views
ScalaClean - full program static analysis at scale
Rory Graves
June 13, 2019 · 10:17 a.m.
463 views
Flare & Lantern: Accelerators for Spark and Deep Learning
Tiark Rompf, Assistant Professor at Purdue University
June 13, 2019 · 10:18 a.m.
380 views
Metaprogramming in Dotty
Nicolas Stucki, Ph.D. student at LAMP
June 13, 2019 · 11:15 a.m.
1250 views
Fast, Simple Concurrency with Scala Native
Richard Whaling, data engineer based in Chicago
June 13, 2019 · 11:16 a.m.
624 views
Pick your number type with Spire
Denis Rosset, postdoctoral researcher at Perimeter Institute
June 13, 2019 · 11:17 a.m.
245 views
Scala.js and WebAssembly, a tale of the dangers of the sea
Sébastien Doeraene, Executive director of the Scala Center
June 13, 2019 · 11:18 a.m.
661 views
Performance tuning Twitter services with Graal and ML
Chris Thalinger, Twitter
June 13, 2019 · 12:15 p.m.
2003 views
Supporting the Scala Ecosystem: Stories from the Line
Justin Pihony, Lightbend
June 13, 2019 · 12:16 p.m.
163 views
Compiling to preserve our privacy
Manohar Jonnalagedda and Jakob Odersky, Inpher
June 13, 2019 · 12:17 p.m.
301 views
Building Scala with Bazel
Natan Silnitsky, wix.com
June 13, 2019 · 12:18 p.m.
565 views
Diversity and Inclusion Panel: Bring the Thunder!
Panel
June 13, 2019 · 2:30 p.m.
244 views
Asynchronous streams in direct style with and without macros
Philipp Haller, KTH Royal Institute of Technology in Stockholm
June 13, 2019 · 3:45 p.m.
304 views
Interactive Computing with Jupyter and Almond
Sören Brunk, USU Software AG
June 13, 2019 · 3:46 p.m.
681 views
Scala best practices I wish someone'd told me about
Nicolas Rinaudo, CTO of Besedo
June 13, 2019 · 3:47 p.m.
2702 views
High performance Privacy By Design using Matryoshka & Spark
Wiem Zine El Abidine and Olivier Girardot, Scala Backend Developer at MOIA / co-founder of Lateral Thoughts
June 13, 2019 · 3:48 p.m.
753 views
Immutable Sequential Maps – Keeping order while hashed
Odd Möller
June 13, 2019 · 4:45 p.m.
276 views
All the fancy things flexible dependency management can do
Alexandre Archambault, engineer at the Scala Center
June 13, 2019 · 4:46 p.m.
389 views
ScalaWebTest - integration testing made easy
Dani Rey, Unic AG
June 13, 2019 · 4:47 p.m.
468 views
Mellite: An Integrated Development Environment for Sound
Hanns Holger Rutz, Institute of Electronic Music and Acoustics (IEM), Graz
June 13, 2019 · 4:48 p.m.
213 views
Closing panel
Panel
June 13, 2019 · 5:54 p.m.
400 views