Skip to content
Hallway
0:00 / 0:00

#tla+#formalspecification#distributedsystems

Leslie Lamport: Thinking Above the Code

Microsoft Research

359K subscribers • 12 videos on Hallway

YouTube
  • Recommended by 8 people: 5 on Hacker News, 1 on Lobsters, 1 in engineering communities and 1 curated list.
  • A classic. People kept recommending it from 2015 to 2026.
  • Presented by Leslie Lamport, creator of TLA+
  • An opinion. It argues one side of a question engineers disagree on.

Intermediate. Assumes working knowledge.

403K views12 years ago8 recommendations

Software designDistributed systemsFormal methods and verificationSoftware architectureConcurrency and parallelism

Leslie Lamport argues that programmers should write rigorous specifications before coding, especially for concurrent and distributed systems.

Architects draw detailed blueprints before a brick is laid or a nail is hammered. Programmers and software engineers seldom do. A blueprint for software is called a specification. The need for extremely rigorous specifications before coding complex or critical systems should be obvious—especially for concurrent and distributed systems. This talk explains why some sort of specification should be written for any software. microsoftfacultysummit.com

Why it's here

8 people recommend this

What people say. Recommended as an essential introduction to the TLA+ mindset and the importance of formal specifications before writing code.

b_fiiveon Hacker News • Recommends

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 link to 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.
View on Hacker News

GeoffWozniakon Lobsters • Recommends

Leslie Lamport: Thinking Above the Code Make sure you stick around for the questions and answers at the end, when things get a little more passionate.
6View on Lobsters

programming-talkscurated list on GitHubRecommends

Under “Software Development”

Thinking Above the Code 00:59:51 by **Leslie Lamport** (2014)
View the list

agentultraon Hacker News • Recommends

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 link to this video
View on Hacker News

discreteeventon Hacker News • Recommends

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. link to this video
View on Hacker News

kedizon Hacker News • Recommends

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: link to 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
View on Hacker News

gobdovanon Hacker News • Recommends

On “Mythical Man Month”

…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: link to this video…
View on Hacker News

u/unixbhaskarin r/emacs • Recommends

Install Emacs on Chrome OS Flex deleted
1View on Reddit

fizixeron Hacker News • Mentions

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: link to this video
View on Hacker News

smnplkon Hacker News • Mentions

On “Testing is a separate skill and that’s why it can be frustrating”

…DD 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 --> link to 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…
View on Hacker News

anaphoron Hacker News • Mentions

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 - link to this video
View on Hacker News

max_on Hacker News • Mentions

On “Software Dev Can't Be Automated – It’s a Creative Process with an Unknown Goal”

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: link to this video
View on Hacker News

xjayon Hacker News • Mentions

On “Tell HN: Dropbox user age verification feature can lock your account”

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 link to this video
View on Hacker News

xjayon Hacker News • Mentions

On “Re-implementing an old DOS game in C++ 17 (2019)”

"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 link to this video
View on Hacker News

antimoanon Hacker News • Mentions

On “The rise of async AI programming”

…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 link to this video 2 link…
View on Hacker News