Leslie Lamport: Thinking Above the Code

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]: [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] [VIDEO]

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 --> [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]

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. [VIDEO]

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] - [VIDEO]

Most of the real world distributed systems would have some videos in some conferences: Spanner: [LINK] Chubby: [LINK] Anything Leslie Lamport: [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]

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]: [VIDEO]

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] [VIDEO]

"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] [VIDEO]

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 [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.

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] [VIDEO] [2] [LINK]

>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: [VIDEO]