Top all-time · #164
Leslie Lamport
Personal blog · lamport.azurewebsites.netprogrammingmath
Leslie Lamport's personal blog at lamport.azurewebsites.net covers programming and math. Since 2017, 251 different Hacker News readers have linked it 391 times, most often “TLA+: design, model, document, and verify concurrent systems”. No feed was found, so read it on the site itself.
Sometimes recommended · 7 of 40 sampled comments recommend it?
Why HN links it
Leslie Lamport's site of papers and TLA+ material on formal specification, state machines, Paxos and clocks. HN readers link it as the source of TLA+ and of ideas such as state machines and Buridan's Principle.
- Recommended for · 7 comments
- One commenter names it the best CS paper of 2017; another says it makes the same point 'more rigorously'; notes have 'interesting commentary'.
Summarised by Claude from a sample of 40 HN comments that link here. Each comment is marked recommending, critical or neutral (citing without judging); how this works.
Most-linked posts?
- TLA+: design, model, document, and verify concurrent systems26 people · 28 mentions · first linked 2017-10-30
- The TLA+ Video Course by Leslie Lamport21 people · 25 mentions · first linked 2017-05-28
- /tla/formal-methods-amazon.pdf21 people · 25 mentions · first linked 2018-07-11
- Time, Clocks, and the Ordering of Events in a Distributed System [pdf]18 people · 18 mentions · first linked 2019-01-27
- Paxos Made Simple (2001)[pdf]11 people · 12 mentions · first linked 2019-08-31
- The Writings of Leslie Lamport11 people · 11 mentions · first linked 2020-05-29
- How to Write a 21st Century Proof (2011) [pdf]10 people · 12 mentions · first linked 2017-11-12
- Specifying Systems (TLA+ Book) out and free for personal use9 people · 10 mentions · first linked 2018-04-02
- Computation and State Machines (2008) [pdf]7 people · 9 mentions · first linked 2018-02-27
- The TLA+ Video Course7 people · 7 mentions · first linked 2017-06-03
What Hacker News says?
> The major rework we need isn't some math theory, some kind of Paxos for Capitalism, or Paxos for Government the part time parliament https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf (lamport 98)
Comment linking /pubs/lamport-paxos.pdf
on “100 years of whatever this will be”Submitted The Paxos Algorithm, or How to Win a Turing Award as a story · 328 points
HN discussionA model checker is a software program you use to validate a given mathematical model of a system. If the proposed properties of the model hold the model checker will let you know. More interestingly if the properties fail to hold you'll get a trace back into where your assumptions fell apart. TLA+ is one such system that includes a language for writing models and a model checker to verify them for you. In the contex…
Comment linking /tla/formal-methods-amazon.pdf
on “Goodbye Microservices: From 100s of problem children to 1 superstar”Submitted Leslie Lamport: Video course on TLA+ as a story · 328 points
HN discussionI read through a chunk of Lamport’s book and the first 7 or so sections of his online course (the rest weren’t posted yet). https://lamport.azurewebsites.net/tla/tla.html https://learntla.com/introduction/ Is also a good introduction. That was enough to make me dangerous. Since work didn’t have an interest in training me, and I had other obligations, that’s all I’ve done so far.
Comment linking /tla/tla.html
on “Learn how to design large-scale systems”Submitted The TLA+ Video Course by Leslie Lamport as a story · 219 points
HN discussionRedundancy. Real answer though it's a Microsoftian's (that's not a word) website https://lamport.azurewebsites.net/
Comment linking /
on “Learn how to design large-scale systems”Submitted The Future of TLA+ [pdf] as a story · 195 points
HN discussionI'd add a section on using TLA+ as a design tool. Diagrams and rules of thumb are useful but they don't catch errors or help you discover the correct architecture. See the Amazon paper [0] on their use of TLA+ in designing (and trouble-shooting) services. [0] https://lamport.azurewebsites.net/tla/formal-methods-amazon....
Comment linking /tla/formal-methods-amazon.pdf
on “Learn how to design large-scale systems”Submitted A Science of Concurrent Programs [pdf] as a story · 187 points
HN discussionI think you are mistaken about this. Vectorizing compilers have been around since at least the late 1970s; the Cray 1[0] had a vectorizing compiler in 1978. Lamport’s Parallel Execution of DO Loops[1] was published in 1974. [0] https://en.m.wikipedia.org/wiki/Cray-1#Software [1] http://lamport.azurewebsites.net/pubs/do-loops.pdf
Comment linking /pubs/do-loops.pdf
on “Frances Allen has died”Submitted The Byzantine Generals Problem (1982) [pdf] as a story · 163 points
HN discussion> I'd say it still appears to be better than fully-impertive "manual" process. I really don’t know. It may largely depend on what you want to do, and I believe Coq also has powerful proof automation, albeit one that works differently. Both take quite a bit of practice to write. The main thing I can say is that TLA+ proofs are easy to read. In any event, formal proofs in any style are far from a walk in the park (whi…
Comment linking /pubs/proof.pdf
on “My unusual hobby”Submitted The Writings of Leslie Lamport as a story · 157 points
HN discussionSure — if and when I get around to writing them :) Looking at your proofs will probably make this a lot easier. After all, the principles of proof are very similar in pretty much every system. But if you want to get a sense of what a methematical proof in TLA+ looks like (as opposed to algorithm proofs, which make up most TLA+ examples), see the appendix to this paper: https://lamport.azurewebsites.net/pubs/proof.pd…
Comment linking /pubs/proof.pdf
on “My unusual hobby”Submitted TLA+: design, model, document, and verify concurrent systems as a story · 148 points
HN discussionLeslie Lamports Paxos protocol has to be in to top 5 algorithms/protocols ( https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf ). This enabled so much progress in computing its unreal.
Comment linking /pubs/lamport-paxos.pdf
on “Ask HN: What's your favorite elegant/beautiful algorithm?”Submitted The Byzantine Generals Problem (1982) [pdf] as a story · 127 points
HN discussionhttps://lamport.azurewebsites.net/pubs/state-machine.pdf
Comment linking /pubs/state-machine.pdf
on “How I Learned to Stop Worrying and Love the State Machine”Submitted The Future of Computing: Logic or Biology (2003) [pdf] as a story · 126 points
HN discussionThere is an interesting and important theorem from control theory that is relevant for this situation. In a paper from 1984, Leslie Lamport has called it Buridan's Principle and phrased it as follows: “ A discrete decision based upon an input having a continuous range of values cannot be made within a bounded length of time. ” The paper is available from: http://lamport.azurewebsites.net/pubs/buridan.pdf It shows th…
Comment linking /pubs/pubs.html
on “Tesla's self driving algorithm's overlay [video]”Submitted A High-Level View of TLA+ as a story · 92 points
HN discussionThe original paper in Section 6 looks at the case of a magnetic field: https://lamport.azurewebsites.net/pubs/buridan.pdf It's a practical issue that affects CPU design, which is also mentioned in the paper under the name "Arbiter Problem".
Comment linking /pubs/buridan.pdf
on “Human brain compresses working memories into low-res ‘summaries’”Submitted Computation and State Machines (2008) [pdf] as a story · 83 points
HN discussion> I guess they need to cotton onto whatever server side change happened and roll it back. "A distributed system is one in which the failure of a computer you didn't even know existed can render your own computer unusable." -- Leslie Lamport, 1987 ( https://lamport.azurewebsites.net/pubs/distributed-system.tx... )
Comment linking /pubs/distributed-system.txt
on “App suddenly crashing on startup due to FBSDKRestrictiveDataFilterManager.m”Submitted A Science of Concurrent Programs (final draft) as a story · 77 points
HN discussionNo, not just for academia. Apparently, Amazon uses it to check their designs for correctness. https://lamport.azurewebsites.net/tla/formal-methods-amazon....
Comment linking /tla/formal-methods-amazon.pdf
on “Software Engineering Within SpaceX”Submitted Bronx High School Math Bulletin (1957) [pdf] as a story · 65 points
HN discussion5 of 9 validator nodes? The Byzantine Generals Problem Leslie Lamport, Robert Shostak, and Marshall Pease (1982) ACM Transactions on Programming Languages and Systems, Vol. 4, No. 3, July 1982, Pages 382-401 https://lamport.azurewebsites.net/pubs/byz.pdf From the abstract: ... It is shown that, using only oral messages, this problem is solvable if and only if more than two-thirds of the generals are loyal; so a sing…
Comment linking /pubs/byz.pdf
on “$625M worth of ETH drained on Axie Infinity's Ronin Network”Submitted Why Don't Computer Scientists Learn Math? (2016) as a story · 64 points
HN discussion
