Leslie Lamport: Thinking Above the Code
Leslie Lamport: Thinking Above the Code on HackerTube: recommended by 5 Hacker News commenters across 5 separate months, 2015–2026.
Leslie Lamport argues that programmers, like architects, should write rigorous specifications before coding, especially for concurrent and distributed systems. The talk introduces the case for writing specs (the TLA+ mindset) as a way of thinking above the code.
What HN commenters said
12 Hacker News comments link this video. Each one links back to its thread.
b_fiiveSep 2022Strongly recommends
I've invested a fair amount of time into learning TLA+, have bought Hillel Wayne's book (Practical TLA+), and found his stuff super valuable. However, if I could do it again, I would have started in the following order: - 1. Watch ▶ this video - 2. Watch all of [link] - 3. Work through examples on [link] I'm normally not a huge fan of YouTube over books / web sites, but in this case the best content comes from Lamport himself, and he's presented it as a YouTube Course. Also, the costume changes are hilarious.
in “Learn TLA+” · View on HN
gobdovanMay 2026Recommends
>He argues that conceptual integrity comes from both simplicity and straightforwardness If you want to follow this advice, I think Leslie Lamport's formulation is the most concrete. His version is: - Write down a small model of what you are about to build before building it. - Try to see how that model could fail. If it still looks good, either make the spec/design doc/model clearer and more concrete, or start writing the code. - If plain text gets too vague, use math. If you want tools to check it, use TLA+ with TLC or Apalache. Quint and stateright.rs are nearby tools in the same area. --- Materials: - TLA+ videocourse by Lamport: [link] - How to win a Turing Award speech: [link] - Thinking above the code: ▶ this video
in “Mythical Man Month” · View on HN
kedizJun 2020Recommends
Most of the real world distributed systems would have some videos in some conferences: Spanner: [link] Chubby: [link] Anything Leslie Lamport: ▶ this video [link] Also the Distributed system course at MIT is fantastic. The labs are also great way to get your hands dirty with distributed system. The link to the class schedule is here: [link]
in “Ask HN: What are some good videos on real implementations of distributed systems” · View on HN
discreteeventSep 2017Recommends
No. Have a look at this video. It's worth it. He's just saying that you should think before you code and that most specifications should be just a few sentences stating what you intend to do. Code as a blueprint is not the same. ▶ this video
in “Programmers who want to change how we code before catastrophe strikes” · View on HN
agentultraMar 2016Recommends
Short answer: try starting with TLA+. I'm working on this. My colleague, who is mentoring me, is the one who's finishing his PhD in software engineering. It's his guidance that has helped me so I don't have a good answer for how to teach yourself yet. We're working on a project to create specifications for Openstack and are learning a lot by working together on how formal specifications could be taught to hackers and developers with no formal mathematics training, etc. If you want a brief introduction to the ideas try some of Leslie Lamports talks on TLA+: [link] ▶ this video
in “Reflections on Programming” · View on HN
antimoanSep 2025Cites it
I think there is a confusion here between Coding and Programming. I think what is described here as "Async Programming" is just programming the way it should be which is different than coding. This is what Leslie Lamport pointed out a while back [1] and recently [2]. According to him programming has 3 stages: 1- Define what task the program should perform 2- Define how the program should do it 3- Writing the code that does it. Most SWEs usually skip to step 3 instead of going through 1 and 2 without giving it much thought, and implement their code iteratively. I think Step 3 also includes testing, review, etc. With AI developers are forced to think about the functionality and the specs of their code to pass it to AI to do the job and can no longer just jump to step 3. For delegating to other devs, the same process is required, senior engineers usually create design docs and pass it to junior engineers. IMO automated verification and code reviews are already part of many developers workflows, so it's nothing new. I get the point of the article though, that there are new requirements for programming and things are different in terms of how folks approach programming. So I do not agree that the method is new or should be called "async", it's the same method with brand new tools. [1] ▶ this video [2] [link]
in “The rise of async AI programming” · View on HN
Show 6 more comments
xjayApr 2022Cites it
Coder sees "We need feature X". Coder implements feature X, marks it as complete; next. So they have the coder (implementer) role covered, but not the "programmer" role ("thinker"/feature designer). Leslie Lamport - Thinking Above the Code: ~ A lot of people like to think that they're thinking, but they don't really do much thinking. [1] Evidently, there was no expectation that the coder/implementer was supposed to do any thinking here. [1] ▶ this video
in “Tell HN: Dropbox user age verification feature can lock your account” · View on HN
xjayApr 2022Cites it
"Writing is nature's way of letting you know how sloppy your thinking is." [1] Dick Guindon "To think, you have to write. If you're thinking without writing, chances are you're fooling yourself. You're only pretending to think." [1] Leslie Lamport [1] ▶ this video
in “Re-implementing an old DOS game in C++ 17 (2019)” · View on HN
max_Aug 2021Cites it
I agree with this perspective. I think people seeking to automate software development should find out a way of compiling something like TLA+[0] to executable code. Right now coders are both masons(brick layers) & architects. TLA+ is what can bee seen as a "blueprint" for code, and the actual code can be thought of as the brick and mortar. Devs having to only focus on the blueprint of the code i.e specifications written in TLA+. Truly takes the industry forward. [0]: ▶ this video
in “Software Dev Can't Be Automated – It’s a Creative Process with an Unknown Goal” · View on HN
anaphorJun 2019Cites it
Leslie Lamport (of Paxos, LaTeX, and TLA+ fame) has been making this point for years. Basically that in order to design a piece of software, you need to be able to create a spec, and the best way of doing that is through mathematics. E.g. - [link] - ▶ this video
in “The Mathematical Hacker (2012)” · View on HN
smnplkMar 2017Cites it
The article is about TDD. You can see on the page, that they are offering a TDD course using ruby/rails. TDD in Ruby community is overhyped. This infection spread to management too. If you apply to Ruby job today, you better have TDD or BDD in your CV. If you don't, you are garbage to them. I have experience with people infected with TDD in ruby land, they often look down on people who don't write tests for every single line of code they write. I am all for unit testing, but can we at least acknowledge that example based testing is just no panacea for bad software. No, easily testable code does not always imply good design. People that don't do TDD are actually doing TDD too, they test code in REPL/console/browser/whatever, they just don't save those "tests". You can not write perfect example based tests, that would cover all possible inputs and states of your system. You need generative testing solutions for this. Let the program write tests for you. [0] [1] See what Leslie Lamport [2] has to say about TDD --> ▶ this video He nearly flips out on the guy :)) Surely Leslie knows what he is talking about. I am ok with unit testing as a communication/documentation tool, so developers know how to use some piece of library. And to prevent regressions with new releases, but I would argue that you can never completely prevent those anyway, requirements change all the time. Maintenance of a large test suite can quickly get out of hand. [0] [link] [1] [link] [2] [link]
in “Testing is a separate skill and that’s why it can be frustrating” · View on HN
fizixerMay 2015Cites it
I saw the TLA+ talk [1] recently and was surprised there was no discussion of code-generation. Once you've spent a significant effort in writing and verifying a formal spec for a program, there should be an automated mapping between it and the implementation, or at least a template of such implementation. [1]: ▶ this video
in “TLA+” · View on HN