Select text to annotate, Click play in YouTube to begin
00:00:01
ladies and gentlemen please welcome judith bishop good afternoon everybody welcome back to the plenary session of the Microsoft faculty summit it's my great pleasure to
00:00:22
introduce to you today Leslie Lamport who's a principal researcher at our Microsoft Research Silicon Valley lab so students and faculty who have taught
00:00:34
operating systems courses as well as anybody who's really used a computer will have benefited from Leslie's work on logical clocks safety and liveness
00:00:45
sequential consistency and many other parts of operating systems which laid the basis for the safe operation of the computers that we have today as they
00:00:58
moved from the single desktop to the large number of interconnected devices we have Leslie before he joined Microsoft was a member of certain various
00:01:12
prestigious institutions he was at MIT at Brandis University and at companies such as Dec Compaq and SR I
00:01:23
in his career he has also received several honorary doctorates and he has tried very hard to help scientists see
00:01:37
their workers beautiful and for that purpose he also developed something that I think you all know very well which is let ik he's now going to go on and try and persuade engineers that there's
00:01:51
something else that is beautiful in life which is mathematics and that's what he's going to talk to us about today so ladies and gentlemen please put your hands together for this year's am Turing
00:02:03
Award winner Leslie Lamport Thank You Judith thinking above the code why do we think well it helps us do most things like hunting a saber-toothed tiger or
00:02:25
building a house or writing a program so when should we think well hunting a saber-toothed tiger we should think before leaving the cave
00:02:39
when the tiger is charging at you it's a little late building a house before beginning construction you don't want to think about what you're doing when the Carpenters are putting the roof
00:02:54
on orally start thinking about what you're doing writing a program we should be thinking before we start writing any code
00:03:06
how to think when I favorite quotes is from the cartoonist Guindon who says writing is nature's way of letting you know how sloppy your thinking is
00:03:20
to think to really think you have to write if you're thinking without writing chances are you're fooling yourself we're only pretending to think
00:03:34
what to write well hunting a saber-toothed tiger sorry writing wasn't invented then which meant it was a very dangerous activity
00:03:46
building a house well what'd you write before you build to start building a house are called blueprints and it's called drawing blueprints writing a program
00:04:00
well you should also write a blueprint of your program but blueprints of programs are what we call specifications specifications
00:04:11
well when I say the word people tend to panic this formal stuff that's possible to read and understand and you have to learn these funny symbols and all that sort of stuff
00:04:25
yeah this is a blueprint you know all these complicated stuff going on but this is also a blueprint in fact there's an entire spectrum of
00:04:38
blueprints ranging from very detailed complicated blueprints which you need if you're building something that's very big and
00:04:49
complicated at the other end they're just rough sketch of what you're building is just something you know really simple that you're gonna do in the weekend and
00:05:01
there are these ordinary blueprints for you know things like a house or the stuff that kinds of blueprints that most of us might have seen
00:05:14
and similarly there's a spectrum of specifications there are formal specifications and on the other end of the your formal
00:05:26
specifications written in a in a precise formal language and on the other and they're just short pro specifications and in the middle are what I like to call mathematical pros
00:05:39
most code is really simple few sentences of prose will do some code is subtle it requires more thought and
00:05:54
for that you have to write it spits prose but it's it try to be you need to be pretty precise and some code is either very complex or very
00:06:09
subtle or critical and that's especially the case if what you're doing is writing concurrent or distributed system it is going to be complex and subtle and quite
00:06:22
likely critical and for that you should have tools you should be using tools to check it to check your blueprints and if you're going to use tools it means
00:06:36
you need a formal language because tools don't understand prose so how to write a spec well writing requires thinking so how to think about
00:06:48
programs we should think about programs like computer scientists namely like scientists scientific thinking is a very successful
00:07:01
way of thinking we know all that it's brought us what science does is make mathematical models of reality for example the first very successful
00:07:14
science was astronomy the reality planets have mountains oceans tides and weather and all sorts of complicating things
00:07:24
but the simple model that's gotten astronomy pretty far is to think of a planet model the planet as a point mass having position and momentum
00:07:40
computer science the reality consists of digital systems things like a processor chip a game console or a computer executing a program this is what I'll be talking about
00:07:55
computer is executing programs but what I have to say applies to all those other things just as well so models there are lots of models that you've probably come across Turing
00:08:09
machines partially ordered set of events you probably haven't run across that and lots of models but - to my mind stand out as being the
00:08:21
most useful basic models functions and sequences of states so functions we model a function of a we can model a
00:08:35
program as a function that map's an input or to an output or multiple inputs - or possible inputs to possible outputs in math the function is very simple it's
00:08:48
an order as a set of ordered pairs so for example the square function on natural numbers it's this set of ordered pairs this pair 0 0 1 1 2 4 etc and the
00:09:03
element 2 4 is an element of this set of the fact that the outlet that the pair 2 4 is an element of this square function is usually expressed by saying square of
00:09:17
2 equals 4 now the domain of of square the domain of a function are all the first elements of those pairs so for the square function the domain is the set
00:09:31
number 0 1 2 & 3 etc also known as the natural numbers that I like to write as net suspect to define a function what you do is you specify its domain so to specify
00:09:46
square we say the domain of square is equal to the set of Naturals and for each element X in its domain we specify
00:09:57
what Square map's X to and it maps the value X to x squared so that defines the square function now functions in math are not the same
00:10:11
as functions in programming languages math is much simpler I'm not a programming language expert so I don't know what those things that programming languages call functions are but I know
00:10:24
what math is that methods are a lot simpler now the functions model will take you very far it's very useful but er has limitations its limitation main limitation is that
00:10:38
it specifies what a program does but not how it does it so for example quick sort and bubble sort compute the same function
00:10:49
but they're very different programs also some programs don't just map inputs to outputs some programs run forever well you know
00:11:01
they may stop before the the Sun explodes but it's useful to think of them it's running forever for example operating systems you can't specify an operating system as a function because it doesn't map inputs to outputs
00:11:15
so for that for those specifications use what I like to call the standard behavioral model in which a program execution is represented by a
00:11:28
behavior a behavior is a sequence of states and a state is an assignment of values to variables
00:11:39
and a program is modeled by a set of behaviors which behaviors that represent all possible executions of the program so for example let's look at Euclid's
00:11:52
algorithm an algorithm is just an abstract program as you all undoubtedly know it computes the greatest common divisor of two natural of two integers m and n by
00:12:05
initializing X 2m and y2 M and then it keeps subtracting the smaller from the larger and when x and y are equal then it stops
00:12:17
because that X and y equals the GCD of M and n so for M equals 12 and N equals 18 there's just one possible behavior it starts with a state in which that
00:12:31
assigns 12 to X and 18 to Y and then subtract the next state is obtained by subtracting the smaller one from the larger X from Y so you get reach a state where x equals 12 and y equals 18 minus
00:12:46
12 or 6 and in the next state you subtract the smaller which is y from the larger and you wind up in the state in which x equals 6 and y equals 6 and since x and y are equal you stop so it's
00:12:59
very simple algorithm it has just one possible behavior so how do we describe a set of behaviors well first of all there's a theorem that
00:13:12
says any set B of behaviors is the conjunct the intersection of two sets a set of behaviors satisfying a safety property and a set of behaviors
00:13:26
satisfying a liveness property so what our safety and liveness well I'm not going to bother going into you know the formal definitions but a safety property is false if and only if it can
00:13:39
be violated at some point during the behavior so partial correctness is an example partial correctness is violated if the program stops with the wrong answer so that's some point in the
00:13:53
behavior you can tell that it that it the property was violated the point at which the program stopped with the incorrect answer the liveness property is one in which you need to see the complete
00:14:06
behavior in order to know if it's false or if it's not satisfied by the by the program classic example is termination you can't tell that the program hasn't
00:14:18
terminated by looking at any finite piece of the program you have to look at the entire behavior to know that it never terminates so we satisfy specify a set of behaviors with by specifying a
00:14:31
safety property and aliveness property now in practice specifying safety just turns out to be more important because that's where errors are most likely to
00:14:43
occur and tend to be more subtle I mean liveness is important just not as important to safety and so to save time I'm going to ignore aliveness today and just talk about safety so how to specify
00:14:57
a safety property we specify it with two things the set of possible initial States and the next state relation which describes all possible successor states
00:15:10
of any state so what language should we use to write these things well let's act like scientists what language do mathema two scientists use and the language is mathematics that's
00:15:24
the language of science so the set of initial states they're described by a formula so in Euclid's algorithm the set of initial States we initialize the initial state is one in which X equals M
00:15:37
and y equals n so that is specified that initial state is specified by this formula and the only part this has only one it's only one possible initial state that satisfies that formula
00:15:51
the next state relation is also described by a formula and to describe it I'll use unprimed variables to talk about the current state or the first
00:16:04
state of the pair and prime variables we're talking about the next state so let's look at the next state relation for Euclid's algorithm there are two possibilities either X is greater than Y
00:16:16
or Y is greater than X so that formula is going to be the disjunction of two of two formulas if X is greater than Y then the new
00:16:28
value of x x prime is equal to what you get by subtracting Y from it so it's new value of x prime is equal to the old value of X minus the old value of y and
00:16:40
the new value of X of Y is equal to the old value so that first formula is specified by all pairs of states satisfying X greater than Y and in the
00:16:54
initial state in first state X prime equals x minus y and y prime equals y were okay you understand what what I said and
00:17:06
that describes one one possibility or the disjunction of these formulas to the other case it's or what Y is greater than X in the first state and the value of y the new state and the value of y in
00:17:19
the old state minus the value of x in the old state etc so this simple formula describes the next state ratio relation of Euclid's algorithm so let's see how it works how you get
00:17:32
behaviors out of those two formulas well for example for an example I'll take em equal to 12 and N equals 18 so to get the initial state we look at the
00:17:44
initial predicate s-- predicate and we substitute 12 for m and 18 for n for what for n rather and you see you under that substitution there's only one pair of
00:17:57
values x and y that satisfy this relation x equals 12 and y equals 18 so to get the next state the second state we apply the next state look
00:18:09
formula substituting 12 for x and 18 for y and we do that notice that 12 greater than 18 is false and 18 greater than 12
00:18:21
is true we'll false and anything is false so that first half of the formula is false true in anything is people to the rest of the formula so this formula
00:18:34
is satisfied by the old value of x being 12 and the new value of x being 18 minus 12 or 6 so this is the only possible next state
00:18:49
that satisfies this next relation when for the initial state x equals 12 and y equals 18 okay to find the next state we do the
00:19:02
same thing we substitute 12 for X and wife and 6 for y we simplify we see that 6 greater than 12 is false and 12 greater than 6 is true so the formula
00:19:15
simplifies to x prime equals 12 minus 6 and y prime equals 6 so it tells us that the only possible successor state the only possible third
00:19:28
state is x equals 6 and y equals 6 and to find the next state well do the same thing we substitute 6 for X and 6 for y and we see that the entire formula is
00:19:42
false and there are no values of x prime and y prime which can make the formula false true so there is no next state so there's no next state means the program is stopped
00:19:54
so that's Euclid's algorithm and when we see special about Euclid's algorithm is for any values of x and y there are unique values of x prime and y prime that make next true there's either
00:20:08
one value or no values so Euclid's algorithm is deterministic to model their non determinism we just have a next state relation that allows
00:20:20
multiple next States for a current state there's nothing magic you know terribly difficult you know hard about can about non determinism multiple assignments of values to prime
00:20:32
variables that make next true for a single assignment of values to unprimed variables that's what non determinism is all about okay what about formal specs
00:20:44
we need formal specifications only to apply tools we mathematicians you know before there were any tools you know wrote math you know very you know an informal notation they want to use
00:20:56
Mathematica though they have to you know write in the language of Mathematica so if we want to apply tools we need a formal language and the language that I'm going to describe were I use is
00:21:08
called TLA plus so this this pair of formulas are written just like this in TLA plus we need to
00:21:22
form a language we need to write declarations we declare X m and n to be constants and x and y to be variables and then add a little boilerplate we said it extends the integers the other
00:21:35
juice or a standard module that defines things like plus and minus and greater than and we put them inside of a module which I've called module Euclid and that's a TL A+ specification of Euclid's
00:21:48
algorithm and this is what it looks like in SK now you can model check TLA plus specs know model checking conceptually checks all possible oceans
00:22:03
of the program on a very small model it's extremely effective and quite easy to do you know you basically
00:22:18
tell the model checker what the model is models are usually you know instantiating values of constants so for Euclid's algorithm we'd have to tell it what m and n equals and then the model checker will go through and in you know
00:22:31
a few nanoseconds for something that simple will we'll check whoa b1 possible their behavior and you can write formal correctness proofs and check them
00:22:43
mechanically in ela you know write the proofs in ela plus and we have a theorem prover that can check the proofs and that's hard work and well all this is math stuff we know he's
00:22:56
you know it's really very well nice and pretty and stuff but we know that math works only for toy examples to model real system you need a real language with types procedures objects and all of
00:23:10
that ma'am wrong let me quote something written by Chris Newcomb as an Amazon engineer said we
00:23:21
have used TL A+ on 10 large complex real-world systems in every case TL A+ has added significant value either preventing subtle serious bugs from
00:23:36
reaching production or giving us enough understanding and confidence to make aggressive performance optimizations without sacrificing correctness one of the other
00:23:50
things people will tell you about formal methods is oh if you use a formal method you're really going to kill your performance well in fact it's just the opposite and the other thing they'll tell you is Oh management will never let
00:24:02
us do it well management at Amazon and now encouraging teams to write TL a-plus specs and in annual planning managers are allocating engineering time to use two
00:24:15
Plus this was written in 2013 I think there are a few more systems that they've been specifying since then the xbox360 memory system a
00:24:29
Chuck Thacker had an intern right at ela plus spec of the Xbox memory system and just writing the spec didn't even get to point of model checking it he caught a
00:24:42
bug that the designers of the memory system at IBM after scratching their heads looking at it said yeah that was a bug and that would not have been caught by their testing procedures and that bug
00:24:58
would have caused every Xbox in the world to crash after four hours of use you can learn about TLA plus on the web today I'm not going to be talking about
00:25:11
TLA plus I'm going to be talking about informal specifications and I'll start with an example TLA Tech which is the pretty printer for TL A+
00:25:23
here is what somebody user TL A+ user might write some silly formula like this and if you just did the naive output you know just you know took things from you know
00:25:36
teletype font and put them into you know translated the ascii into the symbols left / right / into the conjunction symbol and you get something like that formula and the right
00:25:50
but alignment is actually has significance in TL a-plus and the user undoubtedly wanted he certainly wanted the left
00:26:01
conjunction symbols aligned because the formula might mean something different otherwise and he also probably wanted those equal signs aligned so this is the right output that the
00:26:13
pretty partition produce for this example on the other hand if you look at this input this is what the naive output would be like and the user probably
00:26:25
didn't want those two symbols aligned that was probably just an accidental so in this case the naive output is the correct output that's what you want well there's no precise definition of
00:26:39
correct alignment correctness means what the user wants and there's no way of formally specifying what the user wants so obviously if we can specify correctness
00:26:52
specification what good can specification we need to specify correctness what could how can we use specification well we can not knowing what a program should do
00:27:03
doesn't mean you don't have to think you just do this code it means you have to think a lot harder which means that that's what a spec is even more important when you don't know
00:27:17
what the program is supposed to do and it seems impossible to even say what it should do because it has to do something and you have to decide what it should do so that requires a lot of thinking which requires writing
00:27:29
so what did I do well my spec consisted of six rules plus definitions and these are in informal met you know quote mathematical prose
00:27:43
and formal if they're written in comments oh here's an example of one of the rules it says a left comment token is left comment aligned with its covering token well I don't even know
00:27:55
what that means anymore I'd have to read the spec but left comment aligned and covering token are terms that were defined in the in this specification I wrote and if you look at it this is
00:28:09
really mathematical prose what did I write this spec well it was a lot easier to understand and debug six
00:28:21
rules than 850 lines of code probably would have been more than 850 lines of code if I hadn't written those rules first and I did a lot of debugging of the rules you know you write a bunch of rules and
00:28:36
you know what they're going to do is not obvious and you try a bunch of examples and I a debugging code so I could see what rules were being applied and we don't would do with something weird and I say
00:28:50
oh and that rule needs to be modified for this and an iterative process and the few bugs and implementing the rules were easy to catch though there was no problem
00:29:03
had I just written the code it would have taken me much longer to just get something I could live with and I'm sure the results wouldn't have produced formatting nearly as good
00:29:16
so why not a formal spec why didn't I write at tli + spec well several reasons first of all getting it right was not that important the world is not going to come crashing down if something isn't quite properly aligned and pretty
00:29:29
printing in particular it didn't have to work in all corner cases yes No you know there's no way of getting it you know totally right and just as important there aren't any tools that could help
00:29:42
me the model checker wouldn't have helped in this example because you know you need some some properties to check it against and you know they're just tools were not you know the
00:29:56
TLA plus tools are not designed for that kind of problems so what's typical about this spec the spec is at a higher level than the code it could have been implemented in any language
00:30:10
no method or tool none of the fate none of your favorite ways of you know programming methodologies would have been worth a damn here they would not have helped me write the spec
00:30:24
because no method of writing you know better code would have made the spec unnecessary I had to write the spec it was not code and it says nothing about
00:30:41
how to write the code you could implement my spec in any language you write a spec to help you think about the problem before you think about the code
00:30:54
so what's not typical about this spec it's quite subtle remember I said 95% of code people write requires less thought and you know simpler shorter specs good
00:31:07
enough also it's a set of rules a set of rules or requirements or axioms is usually a bad spec because it's really hard to understand it turns out that that was a
00:31:19
good match for this particular problem which says you know there are no universal rules about you know how to write specs you know no universal rules that'll tell you how to
00:31:32
write any program in the world so specifying how to compute a function specifying what the pretty printer should do is hard
00:31:43
implementing the spec was easy specifying what a sorting program should do is easy figuring out how to implement it efficiently is hard at least if nobody has showed you how
00:31:58
it requires thinking which requires writing a specification so I'll give you an example of a specification for quicksort probably you all seen quicksort
00:32:11
quicksort is written by Tony Hoare it's a divide-and-conquer algorithm for sorting an array call it a zero to a n minus one and for simplicity I'll assume that's an array of numbers and it uses a
00:32:24
partition procedure you give it two arguments low and high and what that procedure does is it chooses a pivot point pivot number in low to high minus
00:32:35
1 and then it permutes the elements to the left of the pivot a low to a high at it permutes the number the the part of the array within
00:32:50
the limit from low to high so that everything from pivot downwards is becomes is less than or equal to everything from pivot plus 1 upwards
00:33:04
so fortunately if well seen quits before so i rambling description isn't necessary and for this example I don't care how this procedure is implemented of course
00:33:17
that's the real trick of quicksort implementing that but you know I only have 50 minutes here so so let's specify quicksort and pseudocode you know this by the partition procedure
00:33:30
is pick a pivot and low-to-high -1 and permute a low to a high to make bla bla bla and return the value pivot and you have a recursive procedure q s
00:33:42
applied to low to high and if low is less than high you call the protection procedure for on low and high and then you recursively call the procedure for
00:33:55
the 2 subintervals and if low is not less than high then it means you have one element and there's nothing to sort and so you're done and
00:34:07
the main program just implies Q s to the entire array from Sirte and minus one so informal no formal syntax no
00:34:19
declarations pseudocode it's it's a fine specification yeah when you're gonna code you know pretty trivial to code from this and you know any programming language easy to understand
00:34:32
but it's a really quick sort it's the way quicksort is almost always described but recursion is not a form fundamental part of quicksort it's just one way of
00:34:46
implementing divide and conquer now here's a problem and in fact it's probably not the best way if you want to execute this on multiple cores so here's a problem give to your friends and
00:35:00
colleagues write a non recursive version of quicksort almost no one can do it in ten minutes they try to compile the recursive version and nobody can get almost nobody
00:35:12
can get that right and ten minutes standing on their feet but I'll tell you you know what the real solution is we do is maintain a set u of index
00:35:24
ranges on which partition needs to be called initially u equals contain is a set containing a single index range from zero and minus one
00:35:36
represented by this pair now we can write this in pseudocode but let's be scientists let's write an it and next directly in mathematics so the initial
00:35:49
predicate says a is equal to any array of numbers of length n and u is equal to the set consisting of that single element yep this is in formal
00:36:02
mathematics but it's informal you know we could write some formal way of describing the set of a on any array of numbers of length N and before writing next let me make a definition
00:36:16
let me define partitions of B pivot low high it's the set of arrays obtained from B by permuting the load to be high with
00:36:28
pivot point pivot in other words it's the set of all values that the partition procedure the set of all new values of a that the partition procedure is allowed to return if it's also returning pivot
00:36:43
as the pivot point and I won't bother writing it out precisely so next remember it's going to be a relation between the old values of a of U and the new values a prime and u Prime
00:36:56
so let's write it first of all we're gonna stop if u is the empty set so the next state relation says U is not equal to the empty set and
00:37:08
so performing there's going to be false if u is the empty set then we pick any pair BT in U and if B is not equal to T
00:37:22
then we pick any point P any number P lying in B to t minus 1 and we let a prime be any element of
00:37:34
the set of legal partitions you know the results of the partition function that if you've given it B and T is the input and it returns P as the
00:37:46
partition as the pivot point and then u prime is a set u we're finished with the remai element bTW so we move that from the set and then we add the 2 subintervals
00:38:01
be P and you know to be and P plus 1 to T into the set u of of ranges that still need to be sorted otherwise if B is not e is equal to T
00:38:15
then there's nothing to do we leave a prime unchanged and we let u prime equal u with BT removed we just take BT out of
00:38:28
out of the set and that's the next state relation that describes a very nice way of doing quicksort iterative iteratively it's
00:38:42
actually a more general algorithm because if you look at all the behaviors that can produce the set of behaviors produced by the recursive version is a sub set that is
00:38:54
the set of all sequences of values that a assumes is going to be a subset of the ones that this next state relation allows
00:39:06
so why can almost no one find this version of quicksort because people's minds are stuck in code they haven't thought learn to think at a
00:39:20
higher level than the code now it's easy to write this as a precise formula pick any arbitrary value is really existential
00:39:32
quantification the formula is true if there exists a value B T and you similarly there and just let letting a prime be any element of this set well that's easy enough to
00:39:47
write is a prime and an element of that and those relations new values of U prime those thinks the with pros to the right of the equal sign they're easy to
00:39:59
express whoops this way and so on then so what you have is a TL a plus formula here perfectly formal if you prefer
00:40:21
pseudocode we have plus Cal it looks like a toy programming language and the algorithm in fact appears in a comment and tij plus module but an expression can be any
00:40:35
TL a plus expression it also has some constructs for non determinism but the fact that it can be any TL a an expression can be any TL a plus expression which means any expression of mathematics makes it enormous ly
00:40:49
powerful more more expressive than anything any programming language has designer has ever dreamed of and it gets compiled to an easy-to-understand TL
00:41:01
a-plus spec and in fact I regularly write things in plus cow and then when I'm proving the correctness of them I reason directly about the TLA plus specification and you like the TLA plus
00:41:13
tools the model checker and theorem prover to the plus to the translation programs that run forever have been talking about programs that compute a function programs that run forever usually
00:41:28
involve concurrency things like operating systems distributed systems few people can get them right by just thinking and writing I'm not one of them
00:41:40
we need tools to check what we're doing the reason the TLA plus was so useful to the Amazon engineers is because the model checker
00:41:52
so for concurrent and distributed systems you need to write something you use TLA plus or plus Cal it was designed for distributed systems it's great and you're not gonna get it you know
00:42:06
distributed concurrent algorithm right if you don't model check it it's spent you don't write a specification and check it the other 95% really simple stuff here
00:42:18
is an example of a spec you know that I write wrote in a program why did I write that spec to be sure I knew what the code should do before writing it without writing aspect I only
00:42:33
thought it was obvious what it should do I had to write the spec to be sure it was really as simple and as obvious as I thought it was and later I didn't have
00:42:45
to read the code to know what that piece of code I wrote did I just wrote the specification could rig the specification so a general rule that's one rule at least we can say about specs
00:42:58
in general if you're writing a spec of what a code should do what a piece of code should do that should say everything that anyone needs to know to use the code how the code worked in the example I've
00:43:13
just showed was just too simple to require a spec I mean it was it turned out to be harder than I thought I would have discovered that when I started coding and I would have stopped coding and wrote and written a specification
00:43:26
so what programmers should know about thinking what everyone should know about thinking everyone thinks they think but if you don't write down your thoughts
00:43:39
you're fooling yourself what programmers should know about thinking is that you should think before you code which means you should write before you
00:43:54
code a spec is simply what you write before coating so what coach you know what do I mean by code what should you specify basically any piece of code that someone else
00:44:07
might want to use or modifying and that somebody else is likely to be you in a month when you've forgotten what this piece of code you've written does it could be an entire program or system
00:44:19
a class a method just a tricky piece of code inside of a method what should you specify about the code what it does
00:44:32
which means everything anyone needs to know to use it and perhaps how it does it if it's complicated subtle you need to think hard about in order to get it right
00:44:44
this is you know what's sometimes called an algorithm or a high-level design how should you think about or specify your code
00:44:56
above the code level in terms of states and behaviors or functions for input output relations should do it mathematically as
00:45:08
rigorously informally as is necessary you should be thinking mathematically even if you're writing thing the mathematics very informally perhaps with pseudocode or pass or plus
00:45:23
Cal if you're specifying how something does it so how do you learn to write specs by writing formal specs even if you don't even if you never need
00:45:36
to write a completely formal spec in your life learning to write formal specs will really help you learn to write the informal specs that you need to write you learn to write programs by writing
00:45:49
them running them and correcting your errors you can learn to write formal specs by writing them running them with a model checker and correcting your errors
00:46:00
now TL A+ may not be the best language for you you know it's I'm sure it's not the best language for formal language for every kind of specification in the world no language can be it may not be
00:46:13
the best form of language you know for what your particular needs are but I do know that it's great for learning to think mathematically so unless you can find something better
00:46:24
for doing that you know which works use TL a plus you know learn TL a plus learn to think mathematically how do you connect the spec to the code well you have comments connecting
00:46:40
mathematical concepts and their implementation for example the mathematical concept might be a graph and the implementation would be an array of node objects and an array of link
00:46:51
objects in this connection the other specification especially if it's an informal specification should be in the comments and so should the explanation of how those mathematical comments are
00:47:03
implemented in the code so what about coding I mean we're programs involve writing code you have to write code I have nothing to say about writing code nothing I said implies anything you
00:47:17
still have to think while you code which means you have to write while you're coding but what you're right while you're coding is is code and I have nothing to say about how you should code use any programming language
00:47:30
you want any programming methodology you still you're still going to have to test and debug your program not this good writing aspect is we're going to catch coding errors because it's not
00:47:43
about coding it'll catch algorithm errors writing specs is an additional step and it may save time by catching errors early when they're easier to correct no
00:47:56
promises there it certainly will improve you programming so you'll be writing better programs why are programmers reluctant to write specs well writing is hard writing is
00:48:09
hard in fact because thinking is hard you know there's no Royal Road to mathematics as who wasn't who said that Archimedes I think why is writing hard well because writing
00:48:22
requires thinking and thinking is hard and as I said it's easier to think you're thinking writing is a lot like running unless you do it slower you are and you have to strengthen your writing
00:48:35
muscles you know just like you have to strengthen your rust and you're running muscles it takes practice and it's easier to find an excuse not to and one of the nicest excuses well what
00:48:47
if the spec is wrong maybe you made a mistake in the spec maybe the requirements change where some enhancement is needed in fact and the code will have to be changed
00:48:59
maybe even before the program is finished in fact changing the code is something that eventually happens to all useful programs if your program is useful it's
00:49:13
gonna have users the users are going to find things extra things they want of it the things that don't work the way you know you thought was a good idea be your customers you know decide otherwise this
00:49:25
happens eventually happens to all useful programs in an ideal world you'd write a new spec and then you know the code you'd completely rewrite the span of the spec well we all know this isn't gonna
00:49:38
happen in the real world the code is patched and if you're lucky the spec is updated well if this is inevitable why bother writing specs in the first place if you
00:49:50
know this little lovely thing is you know the spec turns out you know - has to be changed and you know we're back in our old messy world well there's two reasons the first reason is that whoever
00:50:04
has to modify the code will be eternally grateful for every word or formula of specification that you write and whoever maybe you believe me I've you've
00:50:16
done that you know coming back and don't have time for second stories but particularly you know modifications and the pretty print or in fact and that's why you should update the
00:50:29
spec when you change the code the second reason is that every time code is patched it becomes a little uglier harder to understand and harder
00:50:41
to maintain and if you but if you don't start with a spec every piece of code you write is a patch which means the program starts out from
00:50:55
the beginning being ugly hard to understand and hard to maintain and then God help you when you do have to maintain you know try to unfit out what it's doing in order to
00:51:06
to make changes as Dwight Eisenhower said no battle was ever won according to plan but no battle was ever won with that one
00:51:20
so some people will tell you that writing specs is a waste of time in some situations and maybe sometimes there's no need to think about what you're doing maybe something is really so trivial that you know doesn't
00:51:34
need much thought but we'll remember when they're telling you not to write a spec they're telling really telling you not to think and
00:51:45
you know faking is a really good idea and don't trust anybody who tells you not to do it thinking doesn't guarantee that you won't make mistakes but not thinking generally guarantees
00:51:58
that you will find out more about TLA plus go to my home page and click on the link to the TLA web page thank you
00:52:09
[Applause] I think there's time for a few questions very few I think one yeah yes I
00:52:30
hope that's not a judgment on my talk thanks for your talk how about specification by example it's a pragmatic approach that is a little bit inspired by test-driven development
00:52:45
which since it's not complete of course but since completeness anyway is undecidable it's a good pragmatic approach so do you
00:52:58
know so terrible pragmatic approach it's maybe a good maybe a good way to explain what something examples are great to explain them but they're terrible they keep you from thinking you think in
00:53:10
terms of these particular examples the real problem in programming is not to think of your the easy cases the obvious cases the nice case if the hard cases and you don't get that with examples and
00:53:22
boy I'll tell you I you to eclipse programming and I've you know there's so much so many methods of
00:53:32
eclipse that are explained by here's an here's an example of code using it and I have yet to manage to use those methods to do it what I want to do because it
00:53:45
doesn't work I find that it just doesn't work on anything other than that example and I have no idea why not not a program you know programming by example I don't know about you know if that works but a
00:53:56
specification by example it doesn't thank you for the great talk um so what happens once you patch the code do you suggest keeping the old specs around or do you just get rid of him like does it help to have context
00:54:24
well first of all I think whenever I well whenever I do fix bugs and that may require changing the spec I will also take a note as to why I change the spec
00:54:35
because you know two years later I'm going to come back and say why did I do that about whether you know to what extent that's useful for the specification
00:54:47
itself I don't know certainly you're always a good idea not to throw anything away you know we shouldn't be throwing you know information away these days you know it doesn't cost anything to save it so you should certainly save the old
00:55:01
specs whether you should you know whether you should mention the change in the in the new spec I don't I don't have any any good answer to that without wanting to
00:55:21
be rude or anything I think most programmers don't use formal specifications anymore my PhD was in that background most programmers these days they take algorithms they take code they adapt it
00:55:33
to what they want to do and that's 99 percent is from my perspective how most software is built these days that we actually really be nice if it if
00:55:44
that where it can build Bell built well that way it doesn't work because they're trying to use I find that it doesn't work because the other pieces of
00:55:57
code that I want to use don't have specifications so I really can't use them very well I do the best I can and I wind up having to spend a hell of a lot of time
00:56:10
trying to figure out what this piece of code does which something I shouldn't have to do if it had been specified again I've said that you know 95% of programming
00:56:23
you know requires very little specification and you know a few lines you know are usually enough but you know you are going to come up with this 5%
00:56:36
which isn't just you know take this thing and put it here and combine it with this thing there's gonna be something some things code you're gonna have to write that is subtle it has some some a bit of difficulty in it and you
00:56:50
want to be able to you know you want to be prepared for that because we use the same techniques that you use you're the same lack of thought that you use when you're doing that other 95% you're gonna screw up badly
00:57:12
unfortunately I have never really looked into TLA plus but having studied temporal logic it is inevitable to to fail to to notice that that there's a
00:57:25
lot of temporal logic going on underlying what you've been saying so I was wondering have you studied probably you have the possibilities for using more directly the language of temporal logic will
00:57:41
future operates as necessity operators and all that stuff and so ok TLA stands for the temporal logic of actions temporal logic is evil I
00:57:55
can tell you explain why because it's very hard to use but it turns out it's a necessary evil temporal logic turns out to be the best way of thinking about liveness and
00:58:08
so if you use TLA plus when you get to the liveness part you're going to be using temporal logic and be aware of it but remember that I said that safety is more important and it turns out that you do not need to think you got not need to
00:58:23
know temporal logic in order to handle safety and what the reason I think you know that TL A+ is better than other kinds of temporal logic is that you know
00:58:36
ascent need-to-know essentially no temporal logic to use it for safety if you look at the actual specification there is the specific the tli specification I've noticed I've written it it's two formulas in it and next well
00:58:49
TLA allows you to combine them into a single temporal logic formula which you you know you do at the end eventually and but the idea of the thing it makes it great is that you'll write a thousand
00:59:03
line specification 999 lines are going to be ordinary math initial predicate next state relation and then the last line is going to be a temporal logic formula so okay
00:59:16
well do we have no so we are now at the end of our plenary session and I'd like to thank you very much but before we do that just to
00:59:30
remind you all we got the buses outside to go out to the dinner tonight take your bags with you there will be space there for your bags and then we'll be going back to the hotels or coming back
00:59:42
here and now thank you very much Leslie [Applause]
End of transcript