5th HLF – Interviews with mathematics and computer science laureates: Leslie Lamport
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 49 | |
| Author | ||
| License | No Open Access License: German copyright law applies. This film may be used for your own use but it may not be distributed via the internet or passed on to external parties. | |
| Identifiers | 10.5446/40117 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
2
00:00
Internet forumComputerMathematicsDew pointTuring testMusical ensembleComputer animationJSONXMLUML
00:19
Turing testUltraviolet photoelectron spectroscopyQuicksortMultiplication signFrequencyMathematicsComputer scienceRight angleTuring test1 (number)Meeting/Interview
02:10
Turing testTimestampReal numberBayesian networkMessage passingComputer programmingMathematicsAlgorithmMultiplication signState of matterSequenceVideo gameComplex (psychology)Physical systemMusical ensembleMeeting/Interview
07:14
Turing testPhysicistMathematicianExtension (kinesiology)Musical ensembleMultiplication signComputer scienceMeeting/Interview
08:32
Turing testMathematicianTouch typingHypothesisPoint (geometry)QuicksortUtility softwareProcess (computing)NeuroinformatikMeeting/Interview
10:16
Turing testTLA <Logik>Formal verificationAlgorithmNationale Forschungseinrichtung für Informatik und AutomatikData conversionMusical ensembleRankingWeb 2.0Web pageSound effectSeries (mathematics)QuicksortMathematicsLink (knot theory)Field (computer science)Home pageWebsiteVideoconferencingPlanningPosition operatorMultiplication signEndliche ModelltheorieUniform resource locatorComputer programmingRight angleFreewareMeeting/Interview
14:44
Turing testExecution unitComputer programmingFormal languageStudent's t-testObject (grammar)Pointer (computer programming)Flow separationProgramming languageLatent heatSet theoryReal numberObject-oriented programmingImplementationFormal verificationTerm (mathematics)Quicksort1 (number)WordProjective planeMathematicsPhysical systemNeuroinformatikNumerical analysisComputer scienceSemiconductor memorySequenceState of matterMusical ensembleMeeting/Interview
21:35
Turing testMathematicsComputerInternet forumLatent heatMusical ensembleMathematicsAnalytic continuationField (computer science)Meeting/Interview
23:17
Internet forumComputer animationJSON
Transcript: English(auto-generated)
00:22
How many HLFs have you been to this is my fourth right and so you came the first year after you you got the award Yeah Have you seen the changes over the years have you noticed changes or? No, I haven't noticed anything Seemed to recall one year. There was no boat trip
00:43
other than that I haven't observed any Any change it was it was great the first year. I was there and it seems to have stayed more or less the same Yeah, but you do keep coming back. So apparently I like it. Yeah. Well, tell me what you get from it
01:03
Well, I get a chance to Meet with people and talk about computer science and especially the young researchers I Don't Have much contact with Actually, I don't have much contact with other researchers these days and certainly not young ones. Are you still at Microsoft? Yes
01:27
Yeah, by the way, I heard about dr. Thacker, of course Yeah, he's a great guy Occasionally see something
01:40
That I think what you know the newspaper or something and say boy Chuck would enjoy that and then I remember Yeah So actually since we're talking about five-year periods five years ago You you didn't know that you were winning the Turing Award, I guess that was right around the time
02:01
Can you talk about sort of what the what that experience was like going from from then till now? Well suddenly A lot of people wanted me to come and give talks But
02:21
hasn't been any serious change in my life although It did get me to reflect on my career Something I hadn't really thought about much before then And what came out of that?
02:42
I guess Realization of how much I learned from other people in the course of my career The things that
03:01
Wasn't really very aware of at the time For example Thinking back on things I Especially thinking about for example about the work of Edsger Dijkstra. I
03:21
Realized how much I learned From him without without realizing it In the sense that things that I Things that he did and just seemed perfectly natural to me I
03:40
Realized later that he was the first one to do it in particular his way of Reasoning I would say mathematically about Programs as we call them then programs. I think now a little realistic more realistic and the things we were calling programs I think a better called algorithms because they
04:04
Generally didn't have the complexities and you know all the complications that real programs have But you know that work on algorithms has led to Reasoning about real programs these days, but
04:25
Just a way of thinking about it one particular Viewing a an execution of a program as a sequence of states Now that's something that
04:40
It wasn't even mentioned explicitly by Dijkstra that this is what he was doing but if you just look at how the reasoning went it's clear that that was the mathematics that was underlying it and
05:00
I guess now I you know tell people that's the that's the right way to think about Algorithms and systems And It It seems so natural to me that it seems strange when people don't immediately understand it
05:22
So that was one example One thing that I guess reminded me and make me feel a Little more guilty about I may have mentioned it last Time I spoke to you
05:41
That the most famous paper the time clocks paper One of the things it uses time stamps that is Stamps with the Time according to the sender's clock put on the message and
06:03
That idea came from a paper that someone sent me That paper is cited in my in my paper, but I Realized maybe decades later that they invented the idea of using time stamps and
06:23
I Didn't realize I just assumed that oh, this is what everybody did and So now I'm often cited as you know having Original originated the idea of using time stamps and
06:41
feel that it's Unfortunate that you know I didn't Understand that this was a new idea that they had used so I would have mentioned in my paper that you know using the idea of X and Y in You know varying time stamps will do this
07:03
Who was the person do you remember Bob Thomas and? Paul Johnson They were at BBN I believe Did you ever meet either either them or dr. Dykstra? Oh sure?
07:20
Little long I Seen talked to it's her many times over the years I Think I irritated him to a large extent because I
07:42
He had strong ideas, and I had strong ideas and You know I was one of the few computer scientists who weren't intimidated by him Not for any good reason just because I never felt that
08:00
You know it's not like he was a mathematician or a physicist or somebody who did something difficult He just did computer science like I did It's funny that you mentioned his papers, and then the other the time clock papers Which is something that dr. Or said because I asked who are your mentors and he named papers rather than people were there people that you would consider mentors
08:25
Or did you tend to learn more from? The Mentors and people who I think affected me the most Because they got to me when I was younger are not people anyone has heard of
08:47
When I was fresh out of high school and I Really started with working with computers that I had a summer job at Con Edison the electric utility in New York City
09:04
There was someone there whose name. I'm blocking on Norman. I don't even remember his last name He sort of well, I think he recognized that I was smart and
09:21
He he acted as an mentor to me Not mostly in the way of he would give me little puzzles to solve and you know point things out to me and You know I'm not I'm gonna exact exactly sure
09:43
What constitutes mentoring yeah And also I guess I realized my de jure thesis advisor dick Pallet And how much I learned from him and where was that Brandeis graduate school
10:01
You know we've mathematicians have heard of him You know we've become friends over the years Still in touch with them now. You're sort of unusual in a sense that you You're not a professor. You're not Coming into daily contact with with people and again this question of what is mentoring. I guess if I were to say
10:25
You know for the purpose of this conversation Acting as a model of how to think and perhaps out of behavior how to approach problems or something like that Have you been in that position for others besides at the HLF? As I said, I'm not sure what constitutes mentoring, but I've had
10:50
Well I've now someone who's working for me who's Germany and He's been doing programming on the TLA plus tools and
11:06
You Know I try to give him I try to teach him some things so you know as we go along and
11:24
And I worry about you know whether I'm you know he's really getting as much as As he could have you know I'm paying enough attention to Try to to teach him things I've had you know a few
11:41
Young students like that you know a very good intern One year at INRIA and who
12:02
Was sufficiently somehow inspired by what he was doing he was working on on the tools, but he learned from TLA and using mathematics to reason about Algorithms and when he decided to go to grad school he
12:22
Got into he was did it in Verification So I guess I had some effect on him. I hope it was a good one It's not a very fashionable field these days You mean verification is a very fashionable field Actually, let's talk about and I'm just checking the time and then I'll check the questions as well, but let's talk about
12:44
What your passion is now, which I guess you would say is verification and TLA plus Yeah, it's I'm not sure it's so much my passion in the sense that
13:04
It's sort of something that I I Feel I should be doing I think more than other things in my career Because I feel like I have something important to teach to engineers and
13:22
You know, I want to make sure that They get it and it just doesn't get forgotten when I retire So that's why I'm Well making a series of videos on TLA. So They'll have me around even after I do retire
13:43
and Doing the best I can to get tools built and how are those videos and tools available? Go on the website and look for TLA Temporal logic of actions and There's a major, you know, the home page of that and links heading to the videos and the tools and all of that stuff
14:07
well TLA plus actually is Works but works best that will get them to work directly to the right page Imagine TLA stands for a lot of other things. Yes, some less savory brand
14:22
Free letter acronym is my favorite But Actually, I think TLA has been getting up in the web search rankings your TLA. Yeah I think but I I guess I searched TLA plus when I want to find the web page if I don't remember the URL
14:45
So let's so again going back to the five-year theme In your wildest imaginings in your in your most successful dreams, where would you like to see this project go in five years?
15:02
Well my success well the project itself Is I would like to see you know engineers everywhere Well, I'd like engineers everywhere thinking about
15:21
What they're doing before they sit down and start coding and I'd like engineers ones who are building complex distributed systems to be using TLA plus
15:40
Yes Obviously, I think it's great for for that purpose and my real wildest dreams I Would like to see computer science education Change so that
16:04
Students are taught less about programming languages than about What those languages are saying? In particular to think about a computation as a sequence of states and
16:24
That To Understand And what these programming languages were doing in those terms because I have a sense that students these days
16:41
think of programming languages being as being a collection of magic incantations and they sort of have some vague idea of what they do, but not really a clear conception and That's because People don't explain it to them in terms of you know a sequence of states
17:09
For example Object oriented programming object oriented programming is it's it's very nice. You know it has it's
17:21
It's made for better programming languages, but I don't think Beginning students or understand that What they're doing is when they have an object and they're minty of this thing that they call an object is
17:46
Really simply a pointer to some piece of data sitting somewhere and There's a lot of confusion between the pointer and the data it's pointing to
18:04
And The I think that Programming language people Want to think of the object oriented languages as
18:27
Allowing people to think of these wonderful thing called things called objects and not in terms of pointers And a matter of fact you know pointer is a four-letter word. I think in programming languages these days you know because
18:42
C for example is a terribly ugly language because it allows you to do arithmetic on pointers and You know you shouldn't be doing that because you shouldn't you know pointer is sort of pointing you to something But you shouldn't care exactly what that where that thing is or you know what number and memory
19:03
You know that piece of the program and where the data is being stored You should just but you should realize that another word for a pointer might be for a name for it But you should realize that there's a distinction between the name or the pointer and the data that's being named and
19:24
Object-oriented programming languages tend to obscure that distinction and But people are so hung up in languages that you get
19:40
some in real silliness like object-oriented specification languages now specification language Is something that you know specifies? Visually what a program is supposed to do rather than how it does it And so what verification means is that a program?
20:03
Implements its specification it does what a specification says it should do and So somebody I won't name any names You know devised this object-oriented Specification language and
20:21
as he I don't remember what the example was but he gave some example of something written in his language and I realized that It was Much more complicated than it needed to be because it did not make this separation between the up to the
20:44
the name of the of the data and the data itself and so When I you know just that same specification I would nowadays write it in TLA but I it was put even before TLA, but just you know writing it and you know and
21:03
Whatever way I was writing Specifications in those days which wasn't object-oriented so when you to describe the data you Actually had to describe. You know the set of names and the set of things that the names could be naming But having this set of names
21:22
Allowed me to write a much more sensible specification And this was the example you know the first example that he used for how wonderful his you know object-oriented specification language was Is there any final comment you'd like to make just generally about either the forum or about? I know that the topic of mentoring is not one that that you tend to expand on a lot
21:46
but I don't have anything intelligent to say about it well, then the continuity of You know your field and your work I
22:00
Think I feel less the continuity than the change and you know which is great I Just hope that the you know like For example you know I think that
22:22
you know I've learned a lot about writing specifications and What I hope is that people will say oh, yeah, you know you now understand how to write specifications let's go on to do something else and rather than Just have what we've learned forgotten, and you know have to have somebody else reinvented someday
22:43
so yeah, I think I Do tend to see more of a The change than the continuity, and I think it's a good thing Seems like a good place to end. Thank you very much