Microsoft Research
5 HN recommenders · recommended in 11 months, 2015–2026
59:50 · 403K views · Jul 15, 2014
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.
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+.
12 comments from Hacker News
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.
>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
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
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]
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