30 ms·

Leslie Lamport's SCaLE 22x Keynote: Think, Abstract, Then Code Lamport argued for a fundamental shift in programming approach, emphasizing thinking and abstrac

Leslie Lamport's SCaLE 22x Keynote: Think, Abstract, Then Code Lamport argued for a fundamental shift in programming approach, emphasizing thinking and abstraction before coding, applicable to all non-trivial code, not just concurrent systems. Abstraction First: Define an abstract view (the "what" and "how") of your program before writing code. This high-level design clarifies logic and catches errors early. Focus on ideas, not specific languages. Algorithms != Programs: Algorithms are abstract concepts; programs are concrete implementations. Executions as States: Model program executions as sequences of states, where each state's future depends only on its present. This simplifies reasoning, especially for concurrency. Invariants are Crucial: Identify invariants—properties true for all states of all executions. Understanding these is essential for correctness. Precise Specifications Matter: Many library programs lack clear specifications, hindering correct usage, particularly with concurrency. precise, language-independent descriptions of functionality are necessary. Writing is Thinking: Writing forces clarity and exposes sloppy thinking. Thinking improves writing. It's a virtuous cycle. Learn to Abstract: Abstraction is a core skill, central to mathematics. Programmers need to develop this ability. AI for Abstraction? The question was raised whether or not AI models could be utilized for abstract thought processes in programming, due to their seeming nature. The core message: Programming should be a deliberate process of thoughtful design (abstraction) followed by implementation (coding), with a strong emphasis on clear specifications and understanding program behavior through state sequences and invariants. Thinking is always better than not thinking.

neuroelectron 2y ago
Key points: Algorithm vs. Program: An algorithm is a high-level, abstract concept implementable in various programming languages. We should focus on the ideas, not specific languages. Concurrency Challenges: Concurrent programs are hard due to thread interleaving, leading to numerous possible executions. Debugging is unreliable, and changes can expose hidden bugs. Abstraction is Key: Find an abstract view of the program, especially for concurrency, describing how threads synchronize. This higher-level thinking is crucial before coding. All programs: any piece of code that requires thinking before you write code. What and How: For most programs, write both "what" the program does and "how" it does it. Precise languages (like Lamport's TLA+) are vital for verifying concurrent programs but not essential for all. Trivial Example: A simple "max element in array" function illustrates how abstraction simplifies even trivial problems. It revealed a bug in the initial "what" (handling empty arrays) and led to a more robust solution using mathematical concepts (minus infinity). Executions as State Sequences: View program executions as sequences of states, where the next state depends solely on the current one. This simplifies understanding. Invariants: An invariant is a condition true for all states of all executions. Understanding invariants is crucial for proving program correctness. Termination: The example program doesn't always terminate, showcasing the need to consider termination conditions. Real-World TLA+ Usage: Amazon Web Services uses TLA+ to find design flaws before coding, saving time and money. The Rosetta mission's operating system, Virtuoso, used TLA+ for a cleaner architecture and 10x code reduction. Abstraction Beyond Concurrency: Even when the "what" is imprecise (like a pretty-printer), abstraction helps by providing high-level rules, making debugging easier. Thinking and Writing: Thinking requires writing. Writing helps you think better, and vice versa. Learn Abstraction: Abstraction is central to math. Programmers should learn to think abstractly, possibly with guidance from mathematicians. Why Programs Should Have Bugs: Library programs often lack precise descriptions, making them hard to use correctly. This is especially true for concurrent programs where input/output relations aren't sufficient. Lamport emphasizes that programming should be about thoughtful design through abstraction before coding. He advocates viewing executions as state sequences, understanding invariants, and using writing to clarify thinking. He also highlights the importance of precise specifications, especially for library programs. He also touches on the issue of whether or not it is better to outsource abstract thinking to AI.
- fwip 2y ago
  Could we get a policy that just pasted LLM output like this should be labeled?
- School-Cotton 2y ago
  Please just stop posting LLM content to HN. If I want to know what an LLM has to say I can ask it myself.
MrMcCall 2y ago
> Thinking is always better than not thinking. "Truer words were never spoken." --Case from Gibson's Neuromancer
sevensor 2y ago
With all due respect to Dr. Lamport, whose work I greatly admire, I take issue with his example of the max function. The problem he sets up is “what to do with an empty sequence.” He proceeds to handwave the integers and suggest that negative infinity is the right value. But in realistic use cases for max, I want to assume that it produces a finite number, and if the inputs are integral, I expect an integer to pop out. Apologies to Lamport if he addresses this later; this is where I quit watching. There are basically two ways out of this, that I’m aware of: either return an error, or make the initial value of the reduction explicit in the function signature, i.e.: max(x, xs) And not max(xs)
- ndriscoll 2y ago
  I had the same thought skimming the PDF, but he does address it. One of his suggestions is to use an error value as the point at infinity. So I suppose the point is the coding looks the same, but you're taking a more principled view of what you're doing for reasoning purposes.
- tasuki 2y ago
  The answer is a NonEmptySequence type. The `max` function doesn't make sense in the context of an empty sequence.
- pron 2y ago
  > But in realistic use cases for max, I want to assume that it produces a finite number, and if the inputs are integral, I expect an integer to pop out. But that's his point. You're talking about a concrete concern about code, whereas he says that first you should think in abstractions. Negative infinity helps you, in this case, to think in abstractions first.
  - fc417fc802 2y ago
    Are the integers not a reasonable abstraction though?
    - pron 2y ago

neuroelectron 2y ago

Key points: Algorithm vs. Program: An algorithm is a high-level, abstract concept implementable in various programming languages. We should focus on the ideas, not specific languages. Concurrency Challenges: Concurrent programs are hard due to thread interleaving, leading to numerous possible executions. Debugging is unreliable, and changes can expose hidden bugs. Abstraction is Key: Find an abstract view of the program, especially for concurrency, describing how threads synchronize. This higher-level thinking is crucial before coding. All programs: any piece of code that requires thinking before you write code. What and How: For most programs, write both "what" the program does and "how" it does it. Precise languages (like Lamport's TLA+) are vital for verifying concurrent programs but not essential for all. Trivial Example: A simple "max element in array" function illustrates how abstraction simplifies even trivial problems. It revealed a bug in the initial "what" (handling empty arrays) and led to a more robust solution using mathematical concepts (minus infinity). Executions as State Sequences: View program executions as sequences of states, where the next state depends solely on the current one. This simplifies understanding. Invariants: An invariant is a condition true for all states of all executions. Understanding invariants is crucial for proving program correctness. Termination: The example program doesn't always terminate, showcasing the need to consider termination conditions. Real-World TLA+ Usage: Amazon Web Services uses TLA+ to find design flaws before coding, saving time and money. The Rosetta mission's operating system, Virtuoso, used TLA+ for a cleaner architecture and 10x code reduction. Abstraction Beyond Concurrency: Even when the "what" is imprecise (like a pretty-printer), abstraction helps by providing high-level rules, making debugging easier. Thinking and Writing: Thinking requires writing. Writing helps you think better, and vice versa. Learn Abstraction: Abstraction is central to math. Programmers should learn to think abstractly, possibly with guidance from mathematicians. Why Programs Should Have Bugs: Library programs often lack precise descriptions, making them hard to use correctly. This is especially true for concurrent programs where input/output relations aren't sufficient. Lamport emphasizes that programming should be about thoughtful design through abstraction before coding. He advocates viewing executions as state sequences, understanding invariants, and using writing to clarify thinking. He also highlights the importance of precise specifications, especially for library programs. He also touches on the issue of whether or not it is better to outsource abstract thinking to AI.

fwip 2y ago
Could we get a policy that just pasted LLM output like this should be labeled?
School-Cotton 2y ago
Please just stop posting LLM content to HN. If I want to know what an LLM has to say I can ask it myself.

MrMcCall 2y ago

> Thinking is always better than not thinking. "Truer words were never spoken." --Case from Gibson's Neuromancer

sevensor 2y ago

With all due respect to Dr. Lamport, whose work I greatly admire, I take issue with his example of the max function. The problem he sets up is “what to do with an empty sequence.” He proceeds to handwave the integers and suggest that negative infinity is the right value. But in realistic use cases for max, I want to assume that it produces a finite number, and if the inputs are integral, I expect an integer to pop out. Apologies to Lamport if he addresses this later; this is where I quit watching. There are basically two ways out of this, that I’m aware of: either return an error, or make the initial value of the reduction explicit in the function signature, i.e.: max(x, xs) And not max(xs)

ndriscoll 2y ago
I had the same thought skimming the PDF, but he does address it. One of his suggestions is to use an error value as the point at infinity. So I suppose the point is the coding looks the same, but you're taking a more principled view of what you're doing for reasoning purposes.
tasuki 2y ago
The answer is a NonEmptySequence type. The `max` function doesn't make sense in the context of an empty sequence.
pron 2y ago
> But in realistic use cases for max, I want to assume that it produces a finite number, and if the inputs are integral, I expect an integer to pop out. But that's his point. You're talking about a concrete concern about code, whereas he says that first you should think in abstractions. Negative infinity helps you, in this case, to think in abstractions first.
- fc417fc802 2y ago
  Are the integers not a reasonable abstraction though?
  - pron 2y ago