Leslie Lamport: Thinking Above the Code
Why Hacker News recommends it
HN points people to it as Lamport's own case for thinking and writing a spec before coding, and as an entry point to TLA+.
What it is
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.
Recommended by 5 HN commenters across 5 different months, 2015 to 2026.
What Hacker News said
Strong rec b_fiive · 2022-09 · on “Learn TLA+”
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.
Recommends agentultra · 2016-03 · on “Reflections on Programming”
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]
Recommends discreteevent · 2017-09 · on “Programmers who want to change how we code before catastrophe strikes”
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]
Recommends kediz · 2020-06 · on “Ask HN: What are some good videos on real implementations of distributed systems”
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]
Recommends gobdovan · 2026-05 · on “Mythical Man Month”
>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] - Thinkin
Cites fizixer · 2015-05 · on “TLA+”
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]
Cites smnplk · 2017-03 · on “Testing is a separate skill and that’s why it can be frustrating”
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
Cites anaphor · 2019-06 · on “The Mathematical Hacker (2012)”
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]