There is no distributed system without Lamport. His Time, Clocks and Ordering paper to distributed system is like Ted Codd’s A Relational Model paper to database (which is also math!). His elegant analogy between the special relativity, space-time diagram, reasoning distributed systems as state machines, and TLA+; each one is breathtaking.
Paxos is so beautiful. It’s a piece of art. It’s way more elegant and beautiful than Raft (as it solves the smallest consensus problem instead of a log). I will die on this hill.
At the end of explaining the "bakery algorithm", he says "I am proud that I stumbled on it" He doesn't say "I invented it", "I came with it", "I wrote it", etc, etc.
In my career I have seen that people who are true geniuses are also very humble!
Leslie Lamport built Knuth's TeX into the user-friendly version to which he appended the first two letters of his surname: LaTeX. He wrote an excellent, highly accessible guide, LaTeX: A Document Preparation System, which I wish I read before setting off on a thousand random web pages.
His later work prompted me to learn Order Theory, which has turned out to be useful for all sorts of things. Also quite closely related to Category Theory which I wouldn't have had much chance of grokking without first understanding Order Theory, I suspect.
I also used LaTeX heavily in the 80s so was surprised to see him pop up as a genius of distributed systems later (although that work was published much earlier it didn't get much exposure until the 90s). Like "oh that guy must be _really_ smart to excel in two quite different fields".
Great video. I met Leslie once, sat on the bus beside him on the way to a conference around 8 years ago. He wasn't the chattiest, but you bring up his work, he likes to talk. I think he was just over 70 years old, but still incredibly sharp. At the time Microsoft Research were shutting down their valley office, but they would still let him come in there - last one to put the lights out (metaphorically for computer science research at the big IT companies). Nowadays, he couldn't do the research work he did there and at other places at any big IT company - it's R&D, with the emphasis on "D".
I think one of the things that helped was his ability to come up with very catchy explanations and names. “Paxos” and “Byzantine Generals” have great memetic power verses some boring technical name.
In my opinion Lamport is the greatest computing scientist since Dijkstra. His work on the win and sin predicate transformers is grossly neglected and under appreciated. Dijkstra was the first to formalize interrupts and nondeterminism, but Lamport took it to the next level.
Coincidentally I'm also reading about Lamport signature (https://blog.cryptographyengineering.com/2018/04/07/hash-bas...).
It's really interesting because it only uses hash function and doesn't rely on trapdoor function! I think quite many people (me included) only learn about digital signature after public key cryptography, so it's quite a surprise to know about Lamport signature. Also, IIUC, because it doesn't rely on trapdoor function it also resistant against quantum computer in the future
I once carefully read his bio and accomplishments and have felt like a failure ever since.
Something related: https://www.quantamagazine.org/computing-expert-says-program...
Money quote: "When you write an algorithm, you need to have a proof that it's correct. An algorithm without a proof is conjecture, not a theorem."
He says that computer science undergraduates should learn mathematics properly. It is maths that make someone a programmer from a coder.
I am not sure what he means by maths? Exactly which topics in maths?
Again, read SCIP, the best env to do that it's to install Emacs and then, Guile and run:
Alt-x [package-install] (press intro) [geiser-guile]
Alt-x [package-install] sicp
Alt-x [geiser]
Alt-x info (press Intro) Ctrl-s SICP (press Intro).
(Press Ctrl-x b) to switch between the buffers, or just use the menu entry in Emacs.
One of the most interesting results I found in Leslie Lamport's papers is Buridan's Principle:
A discrete decision based upon an input having a continuous range of values cannot be made within a bounded length of time.
Quoting from https://lamport.azurewebsites.net/pubs/buridan.pdf:
"The significance of Buridan’s Principle lies in its warning that decisions may, in rare circumstances, take much longer than expected. Before the problem was recognized by computer designers, some computer systems probably failed regularly (perhaps once or twice a week) because arbiters took longer than expected to reach a decision. Real accidents may occur because people cannot decide in time which of two alternative actions to take, even though either would prevent the accident. Although Buridan’s Principle implies that the possibility of such an accident cannot be eliminated, awareness of the problem could lead to methods for reducing its probability."
In the accompanying notes at https://lamport.azurewebsites.net/pubs/pubs.html, Lamport states:
The four reviews ranged from "This well-written paper is of major philosophical importance" to "This may be an elaborate joke." One of the other reviews was more mildly positive, and the fourth said simply "My feeling is that it is rather superficial." The paper was rejected.