Leslie Lamport, 2013  ACM Turing Award Recipient –  Part 2

Leslie Lamport, 2013 ACM Turing Award Recipient – Part 2


My name is Roy 11 today is November 11th
2016 and I’m at the few Museum in Mountain View California where
I will be interviewing Leslie Lamport for the ACM Turing Award winners project
this is a continuation of an interview that we began on August 12th of this
year Maury Leslie what I’d like to do is pick up the theme that we began in the
last interview we were talking about the different threads of your work and how
they wove together in time and the one that we pursued in some death was just
distributed computing and concurrency what I’d like to do now is to move on
something to the topic that definitely move in with that which is specification
and verification which you’ve worked on it seems to me pretty much all the way
through I think probably because your mathematical background meant that from
the outset you wanted to prove algorithms correct not just create them
I guess last time I didn’t get to the story about the bakery algorithm did I
I’m not sure but why don’t you give it to us now well when I first learned
about the mutual exclusion problem I think it may have been when in 1972 I
believe I joined the ACM and in one of the first edition issues of C ACM that I
received there was a paper giving a new solution to the mutual exclusion problem
and I looked at it I said well that seemed awfully complicated there must be
a simpler solution and I sat down and few minutes I whipped something awful is
a to process solution I sent it to see ACM
and a couple of weeks later I got a reply from the editor who hadn’t
bothered to sent it out to for review saying here’s the bug that taught me a
lesson well had two effects first it made me really mad at myself and I said
I’m going to solve that damn problem and the result of that was the bakery
algorithm but it also made me realize that concurrent algorithms are not
trivial and that we need to have a really good proof of them and so that is
what got me interested in writing proofs and I think it made me different from
most computer scientists who have been working in fields of verification in
that my driving influence has been that I wanted to make sure that the
algorithms that I wrote were correct not only think everyone who was any good and
field of concurrency starting from Dijkstra and who is certainly very good
in it understood the need for writing proofs and so they were writing their
own proofs other computer scientists working upon concurrent algorithms did
not approach the task of a formal method for proving correctness of concurrent
algorithms Dijkstra was interested in correctness of programs but the work of
his that I remember was only on sequential algorithms that is the formal
method and the other early people in the game at Ashcroft wiki and Greece were
interested in formal proofs of concurrent algorithms but weren’t
writing concurrent algorithms themselves so I think I was from the start rather
unique in having a foot in both fields and we’d be fair to say that over the
ensuing decades your approach to a formalization and specification of
algorithms evolved quite considerably Parvat probably as a result of
experience but perhaps due to other factors as well my view of of my progression of ideas was that of a basically a slow process of getting rid
of the corrupting influence of programming languages and getting back
to my roots which was mathematics yeah I want I want to talk about that a little
bit more because I think that’s one of the interesting things and personally
I’ve heard you talk about this quite a bit over the years
the fact that programming languages tend to get in a way of understanding
algorithms and certainly as you just said in terms of proving them correct
maybe if we start as you mentioned at Ashcroft n and the wicked Greece method
maybe if we start by talking a little bit about that and the approach that
they took how it how it influenced you how it contrasted with what you ended up
doing well that craft took a very simple approach of having a single global
invariant which I eventually came to realize was the right way to do things
but Susan and David looking at David grease
and I were influenced by well I was influenced by Floyd’s paper assigning
meaning to programs and they were I think influenced by that and on my horse
work on or logic and we both came up with the same basic idea as in the
Ashcroft method I’m sorry as in the Floyd method
attaching assertions to control points in the program the one difference is
that I realized immediately that the assertions needed to talk not just about
the values variables but also the control state and so right from the
beginning that was encoded in the algorithms working in Greece were under
the influence of whore and I think the programming language community that well
perhaps it’s time to were little digression into what I call the war fee
and syndrome the what is about that last time all I did I don’t know fine then I
would say that awaking briefs suffered from the war fee and syndrome and one symptom of that is that if the
programming language doesn’t give you a way of talking about something it
doesn’t really exist and since the program programming languages didn’t
give you any way of talking about the control state then didn’t exist so you
couldn’t use it so instead they had to introduce auxiliary variables to capture
the control state but what they did is they were really doing and they and I
were really doing a generalization of Floyd’s method but they pretended and I
think perhaps even believed that they were actually generalizing whore’s
method and when they were doing Floyd’s method in core clothing things
got really bizarre I mean how bizarre it is is that they talk about a program
violating a proof of another process but done with the very language and it just
stopped back and see this idea you know a program violating a proof I’m sorry
but you can’t run your payroll program this is because it violates how proof
were before colors theorem but that’s that’s what they talked about as a
result things got awfully confusing and even Dijkstra was not immune to that he
wrote in ewd calling something like you know a personal view of the awaken
grease method you know in which he was explaining it and
yeah I think to the very end Chris was proud of that paper and I looked at it
and said my god how people possibly understand what was
going on reading it from that because if you explain it in terms of the
annotation of the program be a representation of an invariant and then
the basic invariants the basic way you reason about invariant is you show that
each step of the program preserves the invariant and when expressed that way
and it was very obvious when in my approach where the control state was
explicit and in fact in my original paper it explained what the global
invariant was everything is really simple but I think there was a period of
about 10 years when people just really didn’t understand degrees method was all
about and most people are unaware of my paper and that seems to have been sort
of I think it was about ten years afterwards that people started citing my
paper and presumably that med they might have read it and then I think it became
clear to people what was going on and by that time I think I had pretty much
abandoned the idea of scattering the invariant around might you know by
putting it in pieces of the program and just instead writing a global invariant
just like a – Croft had done before us just to clarify from from my own
thinking at the time that all this was going on
which i think was probably in the in the 70s or at least late the late seventies
the focus was chiefly on sequential programs is that right that most of
these methods were we’re not really trying to deal with concurrent programs
so a wiki Greece was dealing with concurrent programs okay that was the
whole thing okay extending both expanding who are
two concurrent programs okay but fourth method was originally intended as a she
was originally as Floyd and hor and originally yes intended for concurrent
for sequential programs actually I came up with a natural generalization the
fours method for apparent algorithms I think I did it
that is I think the original paper was by me and Fred Schneider and I wrote one
or two papers about what I call the generalized sort of logic but I believe
I should check the the record that the original paper was mine and when I sent
that paper to to tell me horror and I wish I had saved the letter in those
days people communicated by letter that Toni replied and he essentially said
when I did the original core logic I figured that it’s extension to
concurrency would look something like what you did and that’s why I never did
it and at the time of course I thought oh
well it all fart you know what does he know but in
retrospect now I agree completely it’s just because I think the global
invariant approach is the best way to do it and the Guru invariant approach
doesn’t particularly single out sequentiality versus concurrency it’s
just an invariant right so that expands those those two areas right well I don’t
think people thought about the Floyd approach in terms of a global invariant
because people were thinking you know one thing at a time so you’re going from
here to there assertion to another and I I’m not sure but I suspect that at
Ashcroft was the one who understood who realized that you know the void method
was a single invariant over now you ended up working with with Susan a wiki
quite a bit subsequently did that grow out of your I won’t i won’t take
conflicting but somewhat differing views about how to do these these things we
said back in the seventies oh what happened is that this was all going on
ran I believe was 77 that I published my paper I think David in Susan’s published
in 76 just got a published a little faster and in 77 I merely published his
paper temporal logic introducing temporal
logic to computer science and Susan who was teaching at Stanford then and she
decided to hold a seminar on temporal logic and my initial reaction to
temporal logic was oh it was just this formal nonsense what they said what the
hell might be interesting and so I attended the the workshop artistical I
guess a seminar and what I came to realize and Susan internalized as well
is that temporal logic was the right way to reason about liveness so for the TV
audience a little digression correctness properties by a correctness property the
kind of properties that I’ve studied and that people usually mean when they talk
about correctness are basically assertions that are true or false of a
single execution of the program that is you can tell whether this property is
satisfied by just looking at a single that a single execution is whether it’s
movable to talk about it being satisfied by this execution for example it never
produces the wrong answer well it’s wrong it you can there’s a behavior an
execution that says you know it produced the wrong answer or it never produces an
answer well we have to look at an infinite behavior but you look at that
one behavior and say it didn’t produce the answer so didn’t satisfy the
property there are other properties like average case behavior for example that
are not correctness properties in that sense so when I talk about correctness
property that’s the property that I mean and it turns out that every property can
be expressed as the conjunction of two different kinds of properties a safety
property which intuitively says that something bad doesn’t happen it doesn’t
produce a bad answer and aliveness property which intuitively says that
something good eventually happens like it terminates and now in my original
paper in the dish the wiki grease method deals only with safety my original paper
dealt with considered safety properties by proof might at that instant we as
invariance properties basically was essentially the same way as a wiki
grease method did but I also had some method for proving liveness properties
and I’m not sure at the time how happy I was with that method but certainly in
retrospect in looking at once temporal logic which they had once on the air had
shown having temporal logic it was clear that temporal logic was the way to
reason about liveness properties because it provided a way to use safety
properties combines improving liveness properties which is something that you
have to do and Susan and I I guess know who were talking about that at the time
and so we published a paper on using temporal logic to prove leibniz
properties the other work on temporal logic that I did was a paper called
sometimes as sometimes not never it makes sense when you put some quotation
marks around children because I realized that there was a confusion going on
because there are actually two different styles of temporal logic equal branching
time and linear time and computer scientists tend to naturally think in
terms of branching time where the whereas ordinary language tends to be
based on linear time the difference is that if you say something is not all
what does it mean to say something is not always false in branching time logic
it means that it’s possible for it to be true and in linear time logic it means
that it must eventually be true and I realized that well the logic that Amir
had introduced was linear time and I realized that that was the right logic
for talking about dealing with safety and I wrote a paper with you know had a
couple of not terribly deeper interesting theorems there and make it
publishable but the basic point of the paper was to to point out those two
different kinds of moderate and to illustrate why I thought that
linear time logic was the right one to be using for proving correctness
properties so you mentioned that Amir used linear time as rather than brown go
ahead yes there’s an amusing and anecdote
about that that was told to me by Dominic mill he who was I believe a
student of Patrick those I’m sorry maybe cannot even get it Patrick Brazeau no
brother Dominic medley oh yes who I believe was a student of Patrick
conserve and when he read my paper he said it was all wrong you know it
doesn’t make any sense and the reason was that he was translating eventually
into the French word advance what our evidence well ek which you know it into
a moon iPhone to a moon in French means possibly and then some what does in
English to you talk about individuality being a possibility so it was misleading
what they were saying it made no sense to him and I’m not sure
how he was Patrick became realized his mistake but when a mere chose to use
linear time rather than branching time do you think that was a conscious choice
because he understood as you came to as well the appropriateness of that for
poor loudness or was this in some sense because it seemed like it was the
intuitive notion of ordinary language so I my understanding and I never confirmed
this with either odd meter or Nissen but that disenfranchise wrote a thesis under
a layer in which he was including properties about concurrent programs but
he was doing it in terms of explicitly talking about time and which meant that
all his formulas had a whole bunch of quantifiers you know for all you know
time T there exists the time you know s greater than T such that for all x u
greater than s blah blah blah and all these quantifiers and Aamir realized
that those particular values are time we’ve had know the interesting thing and
I suppose he must have known a little bit about temporal logic and you realize
that what temporal logic was about was sometimes putting time into the logic so
it did you didn’t have to make it explicit and and I think it must have
been clear that when you translated what what
misson was doing into temporal logic you got linear time temporal logic now I
don’t know how whether I’m here was aware that he was making a conscious
choice of a particular kind of temporal logic I suspect he was because the logic
is using has a name in the literature of temporal logic you know something like
you know something four point five point seven in somebody’s book and I think
that that temporal logicians realized that that was a
a logic in linear time but you know however he got there it was clear that
that was the way to translate what mizzen had been doing so after you and
working with Susan sort of got this idea of applying temporal logic as the
machinery for liveness properties where did that lead next it had no immediate consequence in the
sense that I think it made pretty clear how you would use temporal logic in the
context of doing the kinds of reasoning about programs that you know the wicked
grease method is doing for for safety and how to combine as on safety
properties you know how to use the safety properties various properties
improving aliveness properties well I shouldn’t say that they had no well I
think work of Susan and me had no immediate consequence but our mayor’s
work of course had enormous consequences one of the initial ones that it had was
I think of paper by probably the next I would say important paper on the use of
temporal logic in reasoning about programs who’s talking about programs
was the paper by Richard Schwartz and Mike I’m not your Smith I don’t remember
the name in which they advanced the idea of describing the entire program as with
the temporal logic formula and I was but that idea sounded great
you know we wonderful to be able to just represent the entire program as a single
formula that you could reason about but one that sounded great in principle it
just didn’t work in practice and what I saw was Richard and Michael
and fruits VOC who was who is working with us that I saw her eye for the year
for I believe for a year and they spent about two days trying to write a
temporal logic specification a FIFO queue first didn’t first out I mean the
world’s simplest example of a concurrent system year to process system and they
weren’t able to do it they were able to do it if they made the assumption that
the same element was never put into the queue twice and in fact I think Steve
German remember his name is German a german improving number of years later
that in the temporal logic which they were using which was the original
temporal logic that Amir introduced it was impossible and so they started
people started inventing you know new temporal operators when until operator
you know stab a slide with all the temporal operators and no pudding
suddenly he said you know every other Tuesday and and I just realized that
that was completed work that basically specifying trying to specify I’m not
sure I was aware that it was safety problems that we’re the product that
were the issue but trying to specify safety in temperate with temporal logic
formulas is a loser it doesn’t work because what you wind up doing is
writing a whole bunch of axioms and even if the individual axioms are
comprehensible what you get by combining a whole bunch of axioms you know it is
totally incomprehensible and if you want to see an example of that look at they
some modern specifications of weak memory models and some of them I know
the the Alpha model was one and the Itanium model was another where they
basically specified the possible outcomes from a series of reading write
operations diamond by multiple processes using a bunch of axioms and I’ve seen
people you know puzzle for days over whether you know some particular
sequence of you know two processes usually executing three instructions
whether a particular outcome was allowed by those axioms or not and of course as
you remember from our search days Jim sacks discovered that the original
axiom system for the Alpha permitted cyclic time dependencies where
one process wrote a certain value because another process which read the
value a truly something that allowed it to write that process I realized that
the the only way to describe the safety properties of systems of non-trivial
systems was you know precisely informally it was basically using some
kind of state machines and that’s what programs are if you look at the
semantics of programming languages you know what’s called the operational
semantics which is the only practical ones that that people I think do these
days when they want to build semantics or real programming language they are
describing the how to interpret a program as a state machine so your your
approach essentially evolved to separate the specification of the safety
properties from the special issue specification of the liveness
permanently the latter being with using temporal logic you know former being
state machines and conventional logic I thought things were you know work you
know really well until sometime this in the late 80s I started to write a book
on concurrency and I know I was able to stand at the whiteboard and you know
show you how to pull something and totally convincing you know how you do
the reasoning about the safety properties of using a state machine and
then use tempered logic aliveness properties but when I started writing
something down well when you write something down that really forces you
to do it precisely and when I started doing it precisely I realized it didn’t
work it just didn’t hold together and I don’t
remember exactly you know where things were breaking down at this point but
anyway what that eventually led me to do was to invent TLA which is a temporal
logic and PLA starts with it’s a generalization of our leaders original
temporal logic except everybody else tried to generalize it by using more
complicated temporal operators what I did is that on there is an all other
temporal logic that I know of the fundamental atomic formula building
block that you use for temporal formulas were assertions about a state so the
temporal formula is an assertion about a sequence of states and you built the map
out of fundamental building blocks which are assertions about a single state what
I did in TL a is generalized from an assertion about a single state to an
assertion about pairs of states a state and the next state and that allowed me
basically to write a state machine as a temporal logic formula and so I could
then describe the entire program as a single temporal logic formula except in
a way that really worked in practice so we should probably say that the a stands
for actions which are these years pairs that
that became the basis for your your logic furnace for this kind of reasoning
this is the temporal logic of actions and some people think it stands for
three-letter acronym you probably weren’t thinking about that at the time
but nobody wasn’t so we’re now we’re now in the in the early 90s as that is and
about that time you did some other work that’s in the specification area and it
maybe not directly related but I want to ask you about that because it was a
notion that became quite important and that was refinement mappings work that
you did I think with Martina body you know well refinement mappings started
out being well they’re originally done semantically in which the program should
probably stop calling them programs and this call them systems both because
they’re more general than programs and my interest well what I realize is that
the things that I’ve been calling programs and that other people in
quality programs you know back in the 70s and stuff there weren’t programs
there are algorithms they’re not things that you could throw into a compiler and run and I realized it’s at some point
that back in the seventies and when we started what we were doing or proving
correctness properties of the program in terms of the program itself but that I
realized and other people realized as well that we should really be describing
what the program should do independently of the program and then
prove that the program satisfied the specification now that was one of the
wonderful promises of temporal logic is that if you did that and if the program
could be represented by a temporal formula and the specification could be
represented by a temporal formula then ideally you could proving that the
specification that the program implements the specification really
means proving that the formula that described the program implies the
formula that describes the specification and so you’ve reduced it to a simple
mathematical relation implication but that didn’t work when we couldn’t
describe practice programs or algorithms in terms of you know the temporal logic
that was being used at that time and so you know that idea was sort of was
dropped and when Martine and I were working on refinement mapping we were
looking at the problem of proving that a an algorithm or system implements a
specification when they were both when the safety parts were represented as
state machines and when it would till they came along it
was trivial to turn this semantic approach in terms of state machines into
a formal logical approach and all the reason that we were doing could be done
completely inside of TLA so this idea of refinement mapping has had quite quite
some durability you know I think this early 90s I think when you publish the
paper with the first one with the mark you know I should explain that the idea
of refinement mappings is a generalization of data refinement which
was introduced by Tony Hoare in in these late 70s they’d be around 78 I think any
caller and I think abstraction functions and the difference between a refinement
mapping and an abstraction function which is in some sense the difference
between using about sequential programs and recently about concurrent programs
which is the distinction between your the whole logic and reasoning in terms
of global invariants is that instead of the refinement in abstraction functions
you just look at their mapping at the beginning of the execution and at the
end of the execution but with a refinement mapping you’re doing the that
abstraction function at each step and it has to work at each step got it and as you mentioned this could be done
these refinement mappings could be done completely within TLA yes
and so I imagine that’s what you in fact ended up doing as you continue to use in
developed ela through the 90s well what I was doing in with TLA in the 90s I understood that TLA was the correct
logic for talking and for describing a program but I was still suffering from
the straitjacket of programming languages I hadn’t escaped from that and
my idea is that my original idea was that I would have some specification
language which you know would use visual programming language constructs
assignment statements and stuff like that and then that would be translated
or were as a TLA formula which was then reasoned about but one actually one
significant step came from Jim Horning who said instead of using assignment
statements use I don’t remember what he called them but what an alcohol like now
Colin TLA plus actions rather than you know it’s an assignment being you know
no better you know you sign to the value to a very
new values variable based on you know the court the values of variables in the
current state you just write a relation between old values and new values
very new values so that you know instead of writing X gets X plus one you just
write the new value of x which I now write X prime equals the old value of x
until now right as X plus 1 I think I think German was writing primes and
primes as well as as in fact I had been in in the 1984 paper but I had actually
forgotten about it amusing story that when I published in PLA and talked about
a site using describing semantically actions as relations between primed and
unprimed variables any computer scientist whose name I will not try to
remember said you know I can credit him with that idea because it appeared in
the paper of his and it seemed to me that the idea of using prime variables
and on prime you know for new values and prime very old that for old values you
know let’s go back to the 70s and so I did you know as much of a literature
search as I was going to do and the earliest reference I discovered was a
paper of mine I think 1983 baby boy read that paper anyway
that was I digress so Jim convinced me to try writing than in terms of as
primed and unprimed variables and I figured I would still need a
no bunch of programming language type ideas but I didn’t know which ones so I
decided that I would just just write him in CLA plus and you know when I needed
some programming language construct okay I will I’ll need it use it one of the
things that realization that I had at some point was that I simply assumed
that like any computer scientist does that you have all programming you know a
language it should have types and what I realized is that I didn’t have to add
types into the language and could instead type correctness could be stated
as an invariant and I was wondering them and I was you know so tied to them I
sort of asked Marteen Marteen Abadi well you know I don’t need types because I
can just variants but you know should I use types and Martine said why don’t you
even do it without types that will be more elegant and so I decided I would do
away with types boy was Martine right on that one because what I discovered is that if you do
things try to do things rigorously with types you really either have to you know
I couldn’t do it rigorously with types without enormous ly restricting the
expressiveness and in fact other people you know computer scientists who think
they’re doing things rigorously with types are fooling themselves
at about that time somewhere around the late 80s or early 90s there were three
books that came out that dealt with Bella concurrency with
programs carefully one of them was the misery and Chandi book on unity one of
them was Afghan old rags book on concurrence using about concurrent
programs and the other one was the Greece and Schneider book which is
discrete math but it left a lot about those and they all use type systems and
I came up with this very simple question basically one way of thinking about it
is exactly what is a statement you know X prime equals x minus 1 mean if X is a
type natural and the value of x is 0 and so in other words what does X get X
minus 1 mean and it’s an error that’s not a meaning that’s not know you know
giving something meaning means mathematics and you know you simply
can’t have a mathematics with wither where you have to prove a theorem in
order to determine whether something is it is syntactically legal no that’s
nonsense well neither the champion misra nor the
research neither book answered that question now even though they you know so what
they were doing things you know really rigorously and completely you happened
over drug understood the problem and the way they solved the problem was not
allowing a type natural number they can only have a type integer but it turns out that’s not a problem in
an untied system so when I got rid of types then I was just realized that
mathematics was all I needed I didn’t mean any of these is programming you
know language stuff like types and assignment statements and stuff it
turned out that there are some things that were useful that came from
programming languages for example declaring variables because it turns out
to be useful both you know for parsing for example and it’s a it’s it’s a nice
way of you know sanity checking things and there are other things like way of
splitting things into modules there’s a lot of things a lot of things
mathematics wasn’t well the fundamental problem that mathematics hadn’t really
addressed is how do you deal with formulas that maybe hundreds of lines
long yes mathematicians don’t write them and a specification can be you know a is
really a mathematical formula that’s can be a hundred or you know thousand lines
one which sounds terribly you know if you say that’s improper to program say
on house on line throwing out how can you possibly understand it but if we
tell them oh and thousand line C program oh that’s trivial well C is a hell of a
lot more complicated than mathematics so why did a thousand lines of C program
trivial and you know thousand lines of mathematics not it’s because
mathematicians hadn’t developed you know hadn’t really thought about that problem
and in fact mathematics has the most wonderful method of hierarchical
structure well you deal with complexity like that is hierarchical structure and
math has the most wonderful most powerful hierarchical structure learning
mechanism I know of it’s called the definition I mean if you look at no a
calculus textbook of something you know you get two numbers to the derivative
you know we’re about three definitions or something built on top of one another
so the definition is enormously powerful and in fact mathematicians didn’t even
have an informal definition and the formal notion of a definition like I
don’t know I’m not an expert on logic fact I’m an ignoramus about logic but
the logic books I looked at I’ve never seen any formal definition of a
definition I think the closest they communist is that they will write
definitions as axioms and I don’t like that so I’m going to
introduce the precise notion of the definition and and things and a few
other you know pieces of notation that mathematicians didn’t have for example
mathematicians have no talk about functions but they don’t provide a
practical way of defining a writing a function for example the function whose
domain is the natural numbers that not any number X into X plus 1
there’s no way of writing in ordinary mathematics in a way of writing that
function precisely liberally unless you go to the definition of a function as a
set of ordered pairs which is not a very nice way of doing it great things like
that that I had to add to the language in the language I came up with it’s
called TLA plus and um you just been talking about the fact that
mathematicians typically don’t deal with with these hundreds of lines formulas
but in in the work that you were doing you of course had to in that action
factored led to some some approaches in in how to how to write a formula for
example it’s something you actually published paper about yeah and also you
know how to write proof somewhere along the line I be educated by mathematician
I was under the illusion that the proofs that mathematicians write are logical
and what I came to realize is that the mathematical proof
is literary style that when viewed literally contains a lot of nonsense
things that make no sense but mathematicians learn to read this
literary style and understand the logic behind it non mathematicians don’t and
then they come and that’s a major reason why they can’t learn you know my nan
mathematicians can’t write proofs but also I discovered that in in practice
for writing hand proofs the paragraph style proofs that mathematicians right simply can’t handle the complexity
that’s involved in the kind of proof that you have to write for you know even
a good line a specification that’s in your underlying formula and so I
developed a hierarchical proof structure another way of dealing with the
complexity of big things is is a kind of divide and conquer or what would might
call modularity or decomposition and so on where you build up things from
smaller pieces and put them together and I think you did some work with Martine
again on how you do that with specifications you know I think where
there was a paper well he wrote two to two papers about that I think the second
one was in terms of TLA although he said you know it can be done with any you
know any way of writing specifications I haven’t been working on that because basically the world is far from the
state where the kinds of wood needs to modularize pla plus specifications in
that way that is by writing them as as independent entities that get combined
where so you can sort of add take this specification of you know 5oq
and then you know have it on the shelf and then when you want to use the FIFO
queue inside some something else you just combined it literally with that
specification of the whatever it is you’re building what you you know what
people do these days and what I advocate is that basically if you want to use a
FIFO queue you have a specification of a FIFO queue you basically copy the
relevant pieces of that specification into your current specification and you
know it’s very straightforward you know procedure but no it’s it’s cut
and paste it’s not a modular composition but you know if your biggest
specifications are you know one or two thousand lines cut and paste works fine
also the major tool we have for engineers use for checking TL a-plus
specs as the model checker and that won’t handle specs that are written in
this in that modular style so this leads us in the direction that I wanted to get
to next which is the the practical use of TL a plus and the the tools that one
needs in order to make it useful for for at least some people and that I think
you’ve just touched on that a little bit and the pragmatics of that in particular
needing to have a model checker the model checker came along actually
some time earlier and you worked with several different people over tryman on
that right no no they’re confusing model checker with the oops system there was a
TLP proof system that was the logic TL a CLA not for the language TL a-plus aha
and it was it was quite primitive but it was in some sense a proof of concept
that you really could reason about PL a club about TL a of formulas rigorously
enough that you can you’ll check them with the mechanical theorem improver
okay although you know it was very you know very primitive what happened with
the major tool the model checker is that I was approached by some people in the
hardware group of of I don’t remember whose deck or compact it was probably
compact at the time but but from the old deck people and they were built a cache
coherence algorithm where they were using a cache coherence algorithm that
was the world’s most complicated cache coherence algorithm and they would you
know what did some assurances that it was correct and you know they asked me
and so I volunteered and got you on you and Mark Tuttle and someone you don’t know pull harder who
was not in a in our lab to join me in writing Eddie trying to write a
correctness proof of their cache coherence algorithm when we slaved on
that for six months and all we did was find someone really really tiny bug and
in their algorithm and that’s because those guys who did that algorithm were
incredibly bright unlike some of the people the engineers who came from
compact Houston who tried to build a cache coherence program protocol and
they gave a talk about what they were doing at world our sister lab in Palo
Alto and you know much simpler algorithm and
somebody at the lecture and real-time pointed a toboggan imperative algorithm
but those guys you know the East covers from from Dec were really good but
anyway one was convinced that all of the you know kind of stuff we were doing
should be done by a machine so he decided he was going to write a model
checker and I said Oh couldn’t possibly do it it’s not going to work it’s not
going to be efficient enough but fortunately he ignored many and he went
ahead and did it and and it’s the model checker that has made TLA plus of of
practical interest to engineers so this was this was TLC I have I don’t have an
actual date for when that happened but I think you I think you’re right it must
have been in that really early days of Compaq ownership of deck or baby no that
was around 19 I think 99 okay so right away in that period of
time yeah well not too long before you know you know we left Compaq and so by
this time it is it fair to say that that TL A+ had matured to the point where
other people were at least trying to use it it wasn’t just a tool for you oh yeah
the in fact its first use as it was being written was by in checking the
cache coherence protocol of the EZ 7 the next generation of alpha chip and those
six months that we sweated were not in vain because they gave us cred with the
hardware people and they knew that you know we were willing to put our ass on
her asses on the line and so when we had this model checker the manager I think
it’s managing of testing of the ev7 agreed to assign a junior engineer to
write a TL A+ spec of their algorithm and check it and the those people from
Dec went when Dec sold the hardware the process of business to Intel they went
over to Intel and they started the use of TL a plus at Intel
and it was used for question years there and I’ve lost contact I don’t know if
it’s still being used or not and you will talk about ta+ around this time too
right yeah right
it’s about yes it was after the bottle checker was was written but I think I think it was being written while it
started before the model checker was written so that the book wasn’t based
based around the model checker the way it probably would have been if I hadn’t
written it later you know the model checker was it in a chapter in the book
but the book was about TLA plus but I think in retrospect it’s lucky that I
didn’t appreciate the power and the usefulness of model checking because you
know I was you know thought that you know you need to do proofs because you
know model checking and it might check tiny models and it’s real system I
didn’t appreciate how effective even really tiny models were at finding bugs
and algorithms but the upshot of that was that I designed
TLA plus before the model checker was written and had I and that made it a
much better language because the would have been tempting to do things like ad
types and other things that would make it easier to model check specs as it is
that it was in the early days of handicapped before TLA plus because not
written written for model checking it was much slower to model check than you
know lower level list thus expressive languages that
advantages in way reduced by technology because the cost of the actual
computation has become much much smaller and over the overpowering cost is you
know dealing with the states and writing out to disk and stuff like that so TL A+
is not a big handicap in terms of efficiency of model checking these days
and so the multi-core was a primary tool then in making TL A+ usable by shall we
say mortals but that that wasn’t the end of the story about tools I think that
the system continued to evolve after that can you talk about that whether to
evolutionary steps first the toolbox which is an IDE integrated development
environment basically a GUI for writing TL a-plus specs and I mean I was told by
Gerard Holtzman that when he added the most primitive GUI to his spin model
checker there let hearken did anything to you
the number of users increased by an order of magnitude so I said what should
I do about faster but at any rate and it’s made things a lot easier especially
made it much more convenient to use the model checker
and another thing is we’ve had a proof of project going to be able to write ti+
proofs for and mechanical check them my original interest in that was to give TL
a plus academic cred when thinking that it would be people be more likely to use
it and teach it in universities if there were a theorem prover attached and I was
rather surprised that how good the theorem prover turned out to be and it
was you know I was able to use it to prove you know really non-trivial
verified really non-trivial algorithms and it became even better when we
managed to hook up SMT solvers to it so now forget for proving safety properties
I think it’s it’s it’s practical at least for journal sized algorithms and
in fact you know one journal algorithm was that I was involved with as sort of
the verifier namely I wrote and check the favorite formal proof but actually a
couple of the authors got hooked on it and they you know towards the end they
were you know writing you know parts of the proof too so it’s it’s work but I think it’s it’s not something that you
know that engine engineers will be doing using for I don’t think for the kinds of
algorithms they write although they are interested they would like to because
effective is model checking is there are systems that they build that they can’t
check a large enough model to give them the kind of confidence that they would
like and they would like to be able to write proofs but as far as I know nobody
has in industry has has tried running the proof so have you mentioned academic
cred can you say how that has played out have has in fact TL A+ and it’s in the
system around it come to be used in teaching well I’m afraid it hasn’t the problem is that verification you know
formal specification it is in academia completely separated from the system
building slide of of Education and the most I think most of the courses that
teach specifications is teach specification are actually teaching
specification languages and yet nowadays though you know spend two weeks on TL
a-plus with no as well as all the other massive isn’t it they were due but I
don’t think that students come out with any real experience in in how
specifications can be used in writing real programs building real systems a
little peculiar perhaps in that if if one is studying systems when one learns
about tools for expressing the actual code of that’s of those systems and you
have to obviously have to know about programming languages are going to write
a system and so on but but in terms of the algorithms part of it it seems to be
well actually I should take that back there is a little interest in it for
example the raft algorithm they run a TL A+ back
and and model checked it I think they we’re not terribly terribly satisfied
with it I think there was one bug that it didn’t catch but I’m not sure if it
didn’t catch it because of the model they used or because that is what
because of the spec they wrote or because they couldn’t Jes cannot test
another large enough model but my suspicion is that learning to to write
the kind of abstraction that you need in order to be able to simplify the system
down to learn an algorithm down to its essentials is an art that has to be
learned and I think if you you know if you just try to do something like what
asked it’s your first specification it’s not terribly surprising that you not
going to be able to write a good enough spec to abstract enough spec to be able
to to catch the errors you should be able to catch is that perhaps one of the
one of the problems that are let’s say were the obstacles that to use of
specification technology that that programmers engineers aren’t
sufficiently comfortable with abstraction at the right level well um wanted to think that one time I asked
Brandon Batson who was one of the engineers from deck who went to Intel it
was you know northern responsible for bringing tea li+ there I asked him how
the engineers found using TL a plus and they said something like you know it
takes about a month to forget really familiar with the language and as we
being comfortable with it like any any new programming language but what they
found hard was absent abstract away the details from their specification and and
slowly with use they learned to do that and that ability to abstract improve
their designs and you know he said that with no you know with no prompting but
you know that was music to my ears because my hidden agenda is that the
model checker will will attract the engineers given to start using tli + but
the real benefit the larger benefit is that it teaches them to think abstractly
and to become better system builders and other people have other engineers have
confirmed that that does happen well you wrote a book about on specifying systems
in which abstraction plays a pretty significant role maybe that was even one
of your one of your goals in the book was to help people who have trouble with
that notion of abstraction well I’m not sure I would I would even have
been able to express it in that way that’s one of the things that I’ve come
to realize fairly recently is that the reason that I win a Turing award is for
my talent at abstraction I’m just a lot better than at it than most people and the you know if you look at you know my
most important papers they’re not important because you know I solved some
particular problem they’re important because I discovered some particular
problem I was able to abstract from the unimportant details to get at the heart
of what the real problem was so if you look at instance my time clocks paper
and we’ve written about 40 years ago when the internet didn’t exist you know
distributed systems or than you know we’re a lot different today than they
were now but that paper is still considered relevant for people who
builded mr. Buda distance because he uncovered a fundamental problem and
abstracted it from all of them whole mass of the tales that confront people
when they set out to build a distributed system so while I’m sure that what you
said before about you having an innate ability here is true one might hope that
at least some of this could be taught well I think that it was certainly
developed by studying mathematics because abstraction is what mathematics
is all about yes I’d like to come back to something that you mentioned in
passing well maybe not quite in passing but asked you to amplify a little bit on
it the fact that in the early days you were I don’t think he said hamstrung but
but limited by the fact that you were thinking within the context of
programming languages when and backing off and doing things in the context of
mathematics and not getting hung up on programming languages was was an
important step in somewhat liberating one but it flies in the face of what we
might call the current educational system which doesn’t seem to train
people as well in mathematics as it didn’t perhaps a hundred years ago so
there’s a there’s a tension there that has to be resolved that
the right way to come at specification and thinking about program ins how do we
deal with the fact that people are perhaps not so well equipped well before
I get into philosophical realms let me tell you about something that that I
learned not too long ago the Rosetta spacecraft that until recently was
orbiting a comet in European Space Agency spacecraft had inside of it a
real-time operating system it was named I’m locking on at the moment it’s
controlling of several of the experiments what I learned recently is
that operating system was designed using TLA plus and there’s a book about it
describing the there’s Sensa fication and design process and I wrote to the I
guess was the lead author who was the head of the team that that built that
operating system and asked him about you know with some comments about you know
TLA plus and in an email to me he said that as a result of this system they
built was you know on a second or perhaps later version of an operating
system they had built before and he said wrote to me and said that as a result of
designing it right through the high level design in PLA plus
the new system the amount of code in the new system was ten times less than in
the original system will get a factor of ten reduction in code side size by
thinking in terms of code that’s the short
he also said parenthetically and I’ll try to quote him as accurately as I can
he said we learned the brainwashing effect of ten years of C programming and thinking another example in the packs of salgan
that we discussed I couldn’t have discovered the paxos
algorithm if I had been thinking in terms of coding it and engineers
wouldn’t come up with you know today’s engineers would not have been able to
come up with the paxos algorithm because they’re thinking in terms of code and
you need to think at a higher level well taxes doesn’t solve distributive
systems problems and in fact accesses itself is one reason it’s it’s so
successful is that it’s so abstract and so general that you won’t be able to
define when implementation of it that is suitably efficient in those applications
so you’re going to have to do some kinds of optimizations and if you try just
doing those optimizations at the code level your chances of getting them right
are pretty slim you have to be thinking at the bachelors level at the higher
level above the code level to be able to to have a chance of getting things like
that correctly correct and that’s true whenever you have a more
complex situation you know people believe that a lot of people believe
that if something doesn’t generate code it’s useless well something that
generates code is not going to good if your goal is generating code you don’t
want to be using PLA plus this is not you know it’s going to keep you from
generating code it’s going to allow you to generate less code and I realized
something rather important people think that modern programming languages you
know they allow you to abstract better well programming language constructs allow you to hide information hiding
information is different from abstraction because if you hide what’s
going on inside of a procedure in order to understand what you’ve written
you’re gonna have to know what’s going on inside that procedure and typically
that’s done by you know writing some English no but you know that’s not
precise now can you understand something if you’re not letting it precisely
programming languages do abstract what they abstract from is the hardware you
don’t have to look at the at the silicon to understand what your program does but
you do have to look at the stuff that’s hidden inside that program to understand
it and what the abstraction of TLA plus does it’s not hiding what goes on inside
that procedure it’s being able to express what goes on and you know what
that procedure does in a very simple expression so you can understand it and shall I give you no examples about no
problems that come up with you know not having precise specifications and
certainly I mean I’m just thinking of one could have it recently that bit us
did not I think it was in TL produced the bug in TLC Java has this file class
writing files and it has that class has a delete method you know it deletes a
file and it says it returns true if and only if the delete operation completes
successfully perfectly clear what can be ambiguous about that you see it if the
ambiguous about that seems clear well what happens if you delete a file that
doesn’t exist does that operation succeed or doesn’t succeed well at least
fifteen or twenty years ago two different Java compilers for two
different operating systems had two different answers to that question and imagine first of all try to think about
you know your favorite method and who that you were read about for writing
specifications of Java methods and ask yourself would they have forced
specifier to have answered that question and then how many hundreds or thousands
unanswered questions are there in Java language manual and you get an idea of
how really really really really complicated these simple languages like
Java are I mean my question in proof of that
you know how much simpler that is when people write of a semantics of Java what
they do is they translate Java into mathematics with anybody in their right
mind try to translate math into Java enough said about programming languages and yet at least on one occasion that I
know it may be new in the occasion you tried to make the writing of mathematics
a little bit easier for engineers by giving them if you will a bit of surface
syntax that made it look more like programming yeah you’re talking about
the plus Cal yes language yes which what’s basically like a real simple toy
programming language except that the language of expressions is any TLA plus
expression which means it’s more expressive than more powerful than
anything any programming language designer would ever dream of writing I
mean you can very trivially write a an algorithm it’s I call it an algorithm
language it’s not a programming language you can run a model checker odd that
gets translated at the TLA plus and you can use the TI plus tools to check it
but because the expression language is so simple it’s very easy to write an
algorithm that’s if you know that it says if Goldbach’s conjecture is true do
this else do that very easy to express of course the tools tools wouldn’t
actually have difficulty checking that because when you have a it’s very you’ll
often write specifications in PLI plus in which some number can be any natural
and some variable that have AZ value any natural number and the way you model
check that is you can create a model or one way to do it is you can create a
model for the for TLC that among other things tells it
to substitute some finite sets like the numbers from zero to ten for the set of
natural numbers and so you could that model check that algorithm not
surprisingly for numbers from zero to ten that’s gonna find that Goldbach’s
conjecture is true so so yeah well better know step in the sense that I
wrote it because Keith Marzullo and I were well we were preparing a a course
on concurrency which he actually gave he taught once or twice I forget at UC San
Diego in which you wanted to use white aspects of its algorithms in TLA plus
but he wanted instead of using PLA plus something you know like a toy language
that be translated into t li plus and so I designed plus cow and keith and i
together wrote the plus cal to TL a plus translator and the nice thing about that
is that addition to its being nice a nice introduction to to TL a plus is
that i could publish algorithms in plus cow and computer scientists can could
live with to deal with it because basically the necessary plus calkins
constructs they needed to understand it could be explained in a couple of
sentences so you sort of i call it it’s you know
Plus Cal you should think of as a substitute replacement for pseudocode it
makes pseudocode obsolete it has almost all the best properties of pseudocode in
terms of its expressiveness but you can actually check your your your algorithms
so that’s how how that came about I have conflicting reports about whether
one should teach TL A+ by starting from plus Cal and going up a whether one
should start straight on ela plus and I think my approach is going to be you
know mediate future is for three hidden TL a plus directly I had one more
question I want to ask you about specification and it has to do with one
of the scourges I would say of our of our modern society namely malware and in
general the kinds of security problems that that are a daily occurrence in
modern computing systems there’s a if people made more rigorous use of of
specification technologies and verification technologies of the sort
that you’ve invented do you think we’d be in a different place or could we be
in a different place I am NOT an expert in this my sense is
that the kind of polls but hackers find very low down in the food chain at the
code level and the so the tools of PLA plus is not going to be you’re not going
to be saying oh let’s just apply take TMI plus apply this to this code we’ve
gotten them to find our problems what I think can happen
well first of all if you can reduce your code size by a factor of ten and you
know yes went in many places for hackers to be able to find but it’s not I
shouldn’t give the impression that you know stuff miss D Li plus on your
universal code size by a factor of ten no reason to believe that that’s you
know a normal situation in those just one potato point but what I do believe
is that by learning to think above the code level you will prove your code and
make if less likely that you leave holds your
attacker and I should say tianni pluses is a foreign language I do some
programming and I would say in 10 or 15 years I perhaps used PLA plus or plus
cow maybe a half-dozen times on some method that I’m writing programming in
Java but every method that I write I write a specification for most of the
time it’s in English sometimes with some mathematical formulas if appropriate
but I’m write a specification of what this method it’s supposed to do for two
reasons first of all we’re going to have to do whatever it has to modify that
code is we great you know mother does and that person might be me six months
later in Ellison is but what would is that unless I write down what this
method does I don’t know if I really understand what it does and so this
whole way of thinking improves my coding and you know it’s going to improve many
ones covet who makes the effort of learning tealight less the white and
teal and plus specs you know in a class or something even if he never really
gets a coding job you have a right to TL A+ spec again in his life the or she will use it without realizing
it you need to be writing better code and I’m afraid that with our coding
culture there’s no easy solution to the security problem I fear you’re right what you were just saying led me to
think about what’s actually the next topic I wanted to discuss which is a
different kind of thread that I think has run through your work for decades
again and that is a desire to an interest in communicating clearly and
I’m meaning communication in a broad sense here if I look at you know your
list of papers there are a number in there that talk about how to do things
clearly clear presentations or clear writing the fact that you expend the
effort to design ways of you know structured and hierarchical way present
the mathematics that’s part of your proof systems and and in ela and so on
seems to me another example tools that you’ve built perhaps late acted most
obvious one as a tool for helping people to communicate by not getting caught up
in so much of the detail of form and and I can go on but but it seems to me
there’s a lot of a lot of that that runs through your your work do you have any
any thoughts on on drive to communicate clearly seems to be
underlying a lot of your work I don’t feel it as it tries to
communicate clearly I would say I have a drive to think
clearly and I also happen to be a good technical writer I say good writer but
you know compared to real writers you know in rank amateur but technical
writing is good I’m a good technical writer and part of that I just think
this comes from being a clear thinker and a lot of that is again tied in to my
talent and desire for abstraction because I think if you look at you know
what la tech is it’s it’s abstracted away
a lot of the details of tech so that using latex one thinks about you know
and a higher level above the typesetting level and at the document level that’s
the goal and I don’t think that was written you know – and I mean that was you know so some unconscious are
interested if people communicate better and I think the I mean that I have a
little one and a half page note well how to present a paper which I wrote in mid
70s when I just got tired of the poor presentations
you know seeing people to give at conferences what was the other one that
you mentioned well I was thinking about the the hierarchical proof methodology
and structuring of formulas and so on as another example of how to present things
clearer you talked about the literary style of mathematics and this is in some
sense a pretty big step away from that as a way of being much clearer about
what’s going on well I think much of my work is is not is not
telling people how to showing people how to communicate more clearly but how to
think more clearly so you know how to write approval it’s giving a structure a
logical structure to proofs making them more rigorous and allowing you know
clearer thinking by making it easier to find mistakes but I don’t think of
myself as it is promoting or even practicing clear communication that will in fact I think a problem that I’ve had for much of my
career is not being able to communicate well because I have not understood what
goes on being the way other people think I mean for example I think in a real
disaster that the original Paxos paper was just thinking about that and as I
probably mentioned the one of the jokes in there was that the paper illustrates
things by little scenarios involving people and the people who give them
pseudo Greek names which if you pronounce them out
you figure they’ll ever figure out who the computer scientist I’m talking about
but I figure that even people you know who wouldn’t do that would still be able
to pattern match and I was just surprised by how much that through
readers Christine Christine I think it’s it’s probably something that dates back
to childhood that I never in some sense considered myself really smart but I
didn’t notice that you know other kids I think have an awful hard time
understanding things so if I can if I if I adjust what I was saying
it’s not about clarity and communications about clarity and
thinking you’ve been trying to do as you said and the bat underlies quite a bit
of the work not just in a specification area although that’s an one evident
place for it but in the way you’ve talked about or abstracted work in other
domains as well okay let me throw a quote at you form you
didn’t do it I deny it and I took this from something on your
web page from 2002 you wrote in an email interview to someone quote I think my
most important contribution is my work on writing structured proofs which is
perhaps more relevant to mathematicians than computer scientists in the unlikely
event that I’m remembered a hundred years from now I expect it will be for
that so my question to you is that was written about fifteen years ago let me ask it this way would you tell
revise anything you say well I would simply hold that is evidence at my
inability to predict the future because even once in 15 years later it
sounds a lot less plausible okay to the kid that at the time I said it I think
it should be my painter contribution but mathematicians seem to think otherwise do you think that’s because they just
don’t even L doubt it that it’s you know in some sense in the in the quote wrong
literature for for mathematicians or is it is it the persistence of the more
literary form of proving things that they get taught from an early age well the mathematical community didn’t seem
to have any trouble discovering lay tech yes so you know
things that that appeal to them they get they spread fast so it’s true that not
many people you know I’ve heard of my structured proof method but that’s
because people who have heard about it haven’t told other people about it and
haven’t tried to make it themselves I guess we could speculate on why that
might be but oh I can I certainly don’t have any facts I think the answer is
really simple it’s the psychology is all wrong because what I’m telling people to
do is take theorems that they already believe to be correct and right go to an
effort the effort of writing a more careful proof to find out whether they
really are correct so in the best case scenario with the doing is all this
extra work to verify something they already believe in the worst case
scenario they can go through all this extra work and discover they were wrong
and they have this government who has vanished and you know the referees would
have discovered the error you know if they convinced themselves if
you have to convince themselves so it’s just a lose-lose situation for them you
just have to be really compulsive about not wanting to make a mistake and I
guess another aspect of my career has been that I’m really compulsive about
not making mistakes I want to come back to that interview that you did by email
again because another comment that you made there seems relevant to what you’ve
just said the question that was asked was what is the importance of
specifications and verifications to industry today and how do you think they
will involve evolve over time for example do you believe that more
automated tools will help improve the state of the art and you answer that by
saying there’s a race between the increasing complexity of systems we
build and our ability to develop intellectual tools for understanding
that complexity if the race is won by our tools then systems will eventually
become easier to use and more reliable if not
they will continue to become harder to use and less reliable for all but a
relatively small set of common tasks given how hard thinking is if those
intellectual tools are to succeed they will have to substitute calculation for
thought and your interviewer followed that up by saying are you hinting at
advances in the deployment or artificial intelligence techniques and you said
having to resort to traditional methods of artificial intelligence will be a
sign that we’ve lost the race that was again 15 years ago and the role of
thinking what artificial intelligence bees and how it relates to thinking
seems like an interesting topic to reflect upon how do you think about that
now given a little bit of foot that in
recent months one thing I’ve come to realize is that
some considerable fraction of the programming that’s now done 80% 97% I
don’t know will not not be done by my people because it gonna be done by my
computer’s when this happens again
five years thirty years no I don’t know I think most of it will be done with
current machine learning techniques and that’s going to produce stuff that no
and there’s probably better than you know current programs in that the
machine may wind up with an imperfect understanding of what it is that the
person who’s doing at the task once done but at least that understanding will be
implemented in a bug-free fashion and might even succeed in well I’m not sure that if that will
solve the malware problem or else have a situation in which the the producers of
the software are in no better place than the MAL factors of discovering whether
or not there are holes in it on the other hand that’s not going to be a
satisfactory solution or what I would consider a satisfactory solution to the
problem of getting really reliable software we really care that not that it
just works like most of the time but that it works right essentially all the
time and that’s going to be I don’t think
you’d be able to get that with machine learning because we don’t understand how
machine learning programs work so if we don’t understand you know how they work
how can we understand really what they could get to do you know as long as at
the moment we’re just have to be better than most human beings you know it’s not
a problem so I see two possible scenarios one is that the the use of sophisticated techniques like
machine learning or something will allow translation from precise mathematical
descriptions of what’s supposed to be done to the software in other words the
when is now the above the code level will become the code level by
essentially or learn you know basically will machine learning may replace
conventional compiling techniques to to provide a really higher level of
abstraction the other possible scenario if that
scenario was true that means that you know instead of learning C++ people will
be doing for the birth of the future to do a lot better learning TLA plus the
other scenario is that you know those same machine language techniques that we
don’t understand I’m going to be used to produce software that we should be
understanding and I don’t think that’s going to be a pretty scenario but that
doesn’t mean it won’t happen so you don’t think there’s a fundamental odd
let’s call it conflict between specification of what something ought to
do and machine learning as a technology for getting computers to do something the challenge is perhaps what it means
to be able to say with sufficient precision what a machine learning
program is when that when it is getting the correct answer well I don’t know enough about machine
learning to say anything intelligent about it but if you start I mean what
machine learning seems to be with the good of these days is taking somewhat
vague tasks and doing as good or a better job as a human being and
non-being – at translating those big tasks into something you know that
people have happy with I don’t think it’s been applied to tasks in which what
is to be done is precisely specified and how it gets done is left to the to the
to the program you know hopefully when we’ll be able to come up with ways in which that can be done
sufficiently efficiently and sufficiently accurately to produce the
desired result well that is to make the probability of code being incorrect say
at least as small as it is if you use current code verification and formal
code verification techniques I don’t know how it couldn’t be done but I don’t
know how machine learning is really done nowadays so well does any of this relate
to what is sometimes called probabilistic programming meaning that
instead of there being an answer the answer is expressed with some
probability or some confidence interval or something or like that notions that
we can make precise mathematically but which a little bit different from the
right and wrong absolute distinctions that tend to be made in specifying
programs I don’t think I I would have to guess
what probabilistic programming is about from based on on the word and big thing
that you’re telling me and I don’t think there’s much point ok lying to do that
alright well we don’t have to pursue that come to a somewhat different topic
although it suggested maybe a little bit by something you said earlier having to
do with publication and the notion that that when you go to publish a paper of
course you have to convince some set of referees and editors that result is the
result is worth publishing and sometimes when you’re successful and sometimes not
you have this experience along with everybody else who tries to publish you
if you look at the the system of publishing papers and how it has changed
or hasn’t in the decades that you’ve been publishing how long do you think it
works in and where do we think it’s go where do you think it’s going it’s a
tool for communicating scientific work well
I can’t speak about science I can only speak about computer science computer
and in the past it seems to have worked pretty well I don’t know of any significant work that was inordinately delayed from
recognition because of publication problems in the publication system I mean there I know one isolated incident
instance I’ve when problem life I’ve noticed that he’s in the field of
specification of formal methods is that not know when you mention that that you published something if it’s new it’s
not new you can’t publish it you don’t publish it so if there’s some method
that works you know and you said all there is to say about this there’s some
tendency for just to sink out of sight and people you know will go searching
for you know the literature will come up with all of these ideas that are worse
than that one but they’re the ones that get published I don’t know if this is a
significant problem I mean I can point to one of my papers which I view point
that is being an issue but you know on the whole I’ve been well sort of lightly
publication process but you know I published very little in the
last 5 or 10 years so I really can’t say much about what you know what’s
happening now or is going to happen in the future how about the potentially
transformative effect of self-publishing you talked about the fact just now that
you know people don’t find the thing that works they find it the different
ideas that don’t work seems to me that’s going to be amplified by the ease with
which people can self publish later net or whatever I don’t know perhaps automated things
like reference counts will not be able to take the place of refereeing not a not an issue that I’ve given
thought to there was actually a few years ago that a lot of interesting
so-called reputation systems some which were intended in some way of dealing
with the ease of self publication and the conflict that that poses with more
traditional you know refereed or peer reviewed or something or other sources
that it generally have high reputation but I haven’t seen any of those that
have actually caught on have you seen anything along that plane that you would
well as the h-index yeah I guess that’s probably the main one yeah which is always see bizarre to me because you
know you’re comparing you know you have some formula that involves you know
comparing time with the lens and you know thinking that you get a some
meaningful result out of it you know it’s what is it you know the number of
papers and citations is greater than the rank but why greater than the rank why
not greater than three times the square root of the rank or something there’s
absolutely no justification for it right I have no idea whether anybody has ever
done any study as to you know whether there is you can just simply take that
fully of those two data points and come up with a more reasonable number in
those two there’s two values numbers of I tation and number of published papers published or
something I don’t know it I guess it’s one of these fundamentally difficult problems that
whenever you have any system for judging something you know it’s all it’s always
a substitute for what you’d really like to do measuring you know in some sense
innate quality and whenever med system you use people will be gaining system
rather than improving the quality indeed depressing look true so I think we
actually come to my last question at this point problem which is specifically
about the Turing award and the Turing award is is not a career achievement
award although sometimes it covers a fairly broad space of work so I’d like
to ask you whether winning the Turing award has affected the way you think
about your work and about the impact that it had not necessarily about the
work that you do and assuming that you do the work you want to do whether or
not you win awards but as the fact that you received the award affected your
your the way you think about your work your perspective on your work that’s a tough one because it in some sense I think you’re asking for
is has it changed a rational assessment but I make but it’s very hard to
untangle that from the emotional effects of the award it and then sometimes I think maybe it gets
me to take what I’ve done more seriously and sometimes you think it doesn’t and
then let a lot of the hyperbole that was appearing on especially Microsoft
websites of when I won the award you know credits you know gives me
credit for the development of the internet and if I were to really believe that I would
get really depressed to admit I thought so the effect the negative effects is
the Internet has has had but then good sense comes in and said well that was
really hyperbole I had nothing to do with the existence of another Mohave
internet turned out so I guess the answer is that if you would ask me that question before
I won the Turing award you know you know what is by work been well about or what
good is have been I would been very confused and having won the Turing award
doesn’t make me less confused well if you think back let me push on this just
a little bit more if you think back to the to the year following the
announcement that you had won the award when you were going around giving talks
and and this and that can you recall any any incidents that
occurred during that time as a result of the fact that you were touring as the
current Award winner that stand out and maybe influenced your thinking about it I’m afraid that the give a disappointing
answer us no I mean before I won the award I would will get sort of rock star
treatment and as I went to give a talk you know what it take selfies with the to extent that I guess I always felt a little
uncomfortable about that because people they are the usually students you
know reacting to me as if I think I would have was reacted to for example
two of the speakers that where that came to visit MIT when I was there were niels
bohr and TS Eliot and I mean it seems to me that and I get the sense that they
are regarding me to AG regarded deals bore and TS Eliot and and I said there’s
something wrong there but you know maybe the number of you know students who are
coming up is increased some but I didn’t haven’t felt you know that that to have
changed significantly I think I’ve gotten invitations to the talk from
people who would not have given me an invitation to speak otherwise and those
I’ve politely declined I’m afraid perhaps I was too old by the
time I won at a fraternity would have made the kind of difference that you
seem to be looking for just curious I’m not looking for anything in particular I
just wanted to know we’ve pretty much come to the end of my list of questions
but obviously there are many things in your in your career that we have not had
the time to touch on if there anything that you would particularly like to to
highlight I think this would be a good time to to bring them up well I said I should probably answer a
question that maybe you thought you were answering I’m asking but that I don’t I
don’t think you her which is that one effect that winning the award did have
on me is it got me to look back at my career in ways that I hadn’t and I think
it made me realize the debt that I owed to other computer scientists that I
hadn’t realized before for example I look back it at Dijkstra’s
neutral exclusion paper now I can recognize for decades know what a an
amazing paper that was in terms of you know the insight that he showed both in
recognizing the problem and in stating it so precisely and so accurately but
one thing that I didn’t realize I think until fairly recently is how much of the
whole way of looking at the idea of proving something about an algorithm was
moving that paper he was assuming a an underlying model of computation that I somehow accepting accepted as being
quite natural and I don’t think I understood until recently how much he
created that and I think there are some other instances
like like that where I absorb things from other people without realizing it one of the reasons for that may be that
I never had a a computer science mentor I think I mentioned the mentor I had Con
Ed esand but you know that wasn’t programming and sort of somewhat of a
some bit of intellectual mentor mentoring but I never got that in school
really I never had like a one-on-one relationship with with any professor and
so the whole concept of mentoring is somewhat alien to me I hope that in the
couple of occasions where I’ve been in a position to mentor others I I didn’t do
too bad a job no idea whether I did or not but my mentors have been the my
colleagues and we just learned a lot from them by as Moses and that in
retrospect I’m very grateful for but I was unaware at the time you

Leave a Reply

Your email address will not be published. Required fields are marked *