Leslie Lamport: Thinking Above the Code
Vložit
- čas přidán 1. 05. 2024
- 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.
www.microsoftfacultysummit.com - Věda a technologie
i'm 44 yr old software developer, I thought I was too old. Good to see this.
you are not, you are just on time, keep going!
I started at 42 haha
The approach is incredible… Being fresher and mathematically oriented it’s best to understand the beauty of programming. Thank you for it.
I haven't finished but does it not get boring or tedious?
yeah, Category Theory Does That.....
Talk starts at 2:15
One of the best talk , I have ever heard ...... Great !! Thanks !!
Excelente approach. Clarisima introducción a la ciencia de la computación desde lo menos complejo a lo mas complejo. Buenisimo para alumnos con algo de experiencia en ambitos tecnicos y con ganas de entender y ver un vistazo de lo que es el arte de la programación
Excellent talk. This answered my questions and solved most of my difficulties, Thanks.
Amazing Leslie, thank you for sharing it!
From the Q&A at the end, Leislie seems to say that specifications are a means to 'understand" that a given piece of code does and how it does it without having to parse and test the code. Spatial logics and temporal logics are orthogonal.
He's totally right about a spec by example. This is why the majority of coding tutorials end up being not terribly useful.
The way Leslie's facial expression just falls when he hears the question...xD
Agree. We must learn how to think computationally, beyond simply code
But it is also important to understand the logic, and for the less mathematically inclined, it is often much clearer what the piece of logic is doing when an example is used. However, one must go beyond and generalize the logic back into math after looking at the example.
He's right about specifications by example not working... I find most of the docs online about some language, or framework, or library, usually just cover the easy obvious "hello world" cases. To do anything meaningful and serious, you'll often spend hours combing through third party docs, or stack overflow posts, or even reddit.
That's the main reasons why I never could keep my interest in programming. I've taken programming courses, bought a shit ton of books, but I never had the luxury of associating with other programmer types, and so it was just me, the books (and their boring ass examples) and the Internet (where most everyone can't find the docs they need).
Bingo
@@atlantic_lovewhat do you think about LLMs?
@@jonatan01i Honestly I'm not sure I know what LLMS is
@@atlantic_love chatgpt is an LLM for example (large language model)
Why this great talk is recorded like this? Leslie has very well prepared slides, but we miss most of it.
yep, its wierd
idiots i tell ya
They really need to take care of the details but the only thing Microsoft knows is how to copy Apple.
Slides: www.microsoft.com/en-us/research/wp-content/uploads/2016/07/leslie_lamport.pdf
Yea! I'm getting frustrated at this point!
Very well made and super informative.
Slides: www.microsoft.com/en-us/research/wp-content/uploads/2016/07/leslie_lamport.pdf
Thank you
I work in a consultant company, coding in many languages for many clients and without writing specs, i loss what i code. So, it is a good practice to write down specs in MS Word of what the requirements and then reread again once u need it. Usually I convert the doc to pdf and open with browser and give some colors. Some peoples are good at thinking when given a paper, others are good at thinking when given a gadget ,and else are good at thinking when having nothing (only brain, and draw the thought as a mental image).
You always think with no tool first but it gets lost. You want your thinking translated with the shortest distance into a spec. So it doesnt get lost as quickly.
I write my math research ideas in MS Word as I do the math.
This is something like a gold mine that nobody(at least most) people are missing out on. Mathematical thinking.
It only is impressive to non-mathematicians.
@@bismuti Yeah, as I said, for most people. Most people aren't mathematicians
@@bismuti I'm genuinely interested what did you mean by that? I'm no mathematician. Do you mean it's flawed or worthless?
Very good talk,. Much of the code out there is like a vortex. Siren code
23:51 what's the use of performance if you can't provide accurate answers. Nonetheless, using states and behavior does provide more room for performance, tho I think certain formal method maybe requires certain code structure to verify the correctness
Prolog code resembles TLA+ a lot (conceptually; not syntax-wise), at least when correctly written in declarative form ("pure" Prolog, using CLP, etc). So I think we can say such Prolog programs are both the specification *and* the executable code at the same time. Of course, writing good Prolog has a long learning curve because of the required inherent logical correctness.
Hi i am a beginner in programming, do you have some advice for me?
When I envision a mad scientist. A computer master. I envision Leslie Lamport.
Excellent talk :-)
"function in math is very different than functions in programming languages..." I used to think so too...but then I met Haskell!
It's inherent for me to write code before thinking. But the times when I have thought before writing code I got it right at the first attempt.
masterpiece thinking!
"6 Specs are better to understand than a 800 line code..." This is cool...!!!
amazing explanations.
Is there a link to slides?
the quickest method for giving yourself away as someone who did not understand a word of what was said here is to compare this to TDD
That is true except for the property based testing where you basically defining the spec and let the test framework come up with random examples.
Here is the slides PDF www.microsoft.com/en-us/research/wp-content/uploads/2016/07/leslie_lamport.pdf
@ 33 min. mark Quick Sort description resembles 7 year old Carl Gauss' devised strategy to quickly sum all integers from 1 to 100, by pairing them
- in effect, folding in half, the imagined single-file "stack" of all those numerals. (right?)
which it seems is the process described in Mr. Lamport's Partition Procedure in the described Code Specification.
Maybe only at the first look. He basically devised a formula which can be applied directly, while algorithms usually have to be computed by reducing the problem iteratively, I.e. not in one step. Quick sort is a divide and conquer algorithm which has many similarities with other algorithms of this type.
I don't see the relation. The pivot point is basically randomingly chosen. If it falls into the middle that's just by chance. Of course in actual implementations you may find more deterministic ways to select a pivot, but that's not under discussion here.
@@bitti1975 Because I don't think tradeoffs at pivot choice was the point he was trying to argue for
wondering how we can write specs for features of a frontend and backend system
One architectural approach is to use behavior driven development techniques like collectively writing gherkins with the business using a syntax referred to as gherkin. Another is to write your unit and integration tests before you write your code. Review this as a team before coding begins. This is referred to as test driven development. Another is not writing specifications and relying on the team to collectively produce fluent code. This requires group design sessions with one person coding and the rest of the team collaborating. Retroactively note any design decisions in an architectural decision record directly in the code repository.
@@eric321ification Leslie mentioned that unit test and integration test are "how to code" and implementation details.
I'm thinking more along the line with task1, "the what your code to do". We can consider the frontend a complicated state machine especially when using react.
This week I will be re reading Joel's Software blog about writing specification. I will be trying to bridge Joel and Leslie's advice on writing "spec" and try to level up my frontend and backend. Will be an interesting challenge
I'm a little late here but:
Note how he talks at the beginning about mixing up coding and programming. Keep that in mind, how coding is akin to typing.
Next, he says most programmers get stuck on the code and are not thinking, and that to think you MUST WRITE (which is debatable, and I will debate it).
Then, he talks about this language he writes his thoughts on before actually coding.
Now, remember coding is writing? so programmers that jump straight to coding... aren't they writing down their thoughts already?
People don't use the fast version of the QS code not because they're thinking in code, it's because they're thinking in recursion, which is WAY simpler than the iterative version of this algorithm. Even in the slides I'm sure it went over people's heads, while the recursive version never does. There is nothing stopping you from thinking and writing the iterative version straight to code, except that it's harder to think about it, on a napkin, blackboard or terminal.
Oh but it's writing in a programming language so it's different? how so? there's PLENTY of work on code generators that take a spec and turn it to code. It's just a domain specific language. There's even a large (and somewhat misguided, admittedly) movement around "the code IS the spec".
It seems to me his TLA+ is just a domain specific language where it's easier to express the kind of thoughts that are difficult in other languages, so just as for trivial coding you'll just write it out without much effort, in TLA+ you'll be able to write out a different kind of code in the same fashion, then hand compile it down to the language your sistem is being written in.
While it's hard to argue against thinking, I do argue against specs because they tend to be out of sync, just because they are two separate pieces of data. Domain specific languages are really cool and I've used a couple, but they're not easy to integrate. All code should be readable and a DSL could help make the hard code more readable. Until we get there, I'd echo the advice of writing specs for the hard bits, but in comments near the code itself, for future you or some other poor soul that has to maintain what you wrote.
And for gods sake, write a user guide for your library, don't make me read a spec (or god forbid, the implementation itself) for basic usage!
TL;DR: mathematicians prefer math notation to code and believe it's objectively better.
Programming is like the work of a film director when he works on thinking before applying
Very interesting its something l like it and if l have the opportunity l would like to work to find a job to these computers and math its great l love it
What a legend.
Is this lecture in South Africa?
He's the guy who gave us confortable condoms, right?
why (0,0) was in ordered pairs, for the square function on Natural numbers ? and he also considered 0 in domain.
Many Mathematicians include 0 in the definition of natural Numbers since then they form a monoid with the + operation which makes them more useful.
very easy, go read wiki on math relations (3, 9), 3 is the input, 3*3 = 9 is the output but math write them in a pair . here is many pairs : (0,0), (1,1), (2,4), (3,9). Domain just means a range of input which is left of the pairs above: 0, 1, 2, 3. But I think I got your question about 0. 0 is thought by some to be in natural number. Because you can fold down all fingers and got 0 finger (this could be easily understood naturally 1000+ years ago)!
*Audience says great talk and then they show they didn't understand a single word. I feel sorry for Lampart. No wonder he exploded in the Q&A session at the end of the talk.*
These ivory tower “thinkers” are ignorant and clumsy sociopaths.😊
Been using LaTeX since 2006 if I remember correclty. I've always thought Leslie was a woman! What a surprise I got today!
Also, the talk was way above my level, but it was interesting to listen.
Holy heck, the guy has 9000 slides and clicks constantly and the cameras just won't leave him. Show the darn screen. Was 2014 the stone-age of production value? >:E
www.microsoft.com/en-us/research/wp-content/uploads/2016/07/leslie_lamport.pdf
>:3
chill bruh
They show the relevant text when he is talking about it... If you want to just download the slideshow on its own, maybe write to him and ask him for it (it has been a while but who knows). He also does not have that many slides - you are probably interpreting the slide overlays as new slides, and even then, he explains literally everything in words. Or pause the video on the slides if you need to.
@@spde slides above 👆
Bookmark: 13:00
Can I just use your blueprints?
No royal road to math? I think was Gauss?? XD. Amazing and inspiring talk by the way
I think Euclid
1:41 i didnt expect ms would cention latex in its presentations
Lol when that first guy asked about specification by example I IRL facepalmed
The scientific problem in natural systems is that the state variables are seldom known. Or, putting it more positively, have to be discovered.
I didn’t understand it but this guy is awesome!!!
thanks a lot. this is super useful to me.
how dare you impersonate me!
Ty
I am hooked on TLA+
for thinking we have to writing
He is like Steve Jobs, but with a different shirt.
pensavo bene comunque, la presenza stessa di un qualche servizio qualsiasi è intesa come ordine, anche se sotto forma di ricerca e/o sperimentale, e in particolare talvolta anche in sostituzione di qualcosa di precedente. e qualcuno ha fatto er boom per questo.
in quanto tali servizi non erano richiesti da nessuno, manco il finto governo non votato o la chiesa messa là a far finta di leggere i sermoni come se non fosse tutta una struttura di controllo mentale
la madonnina che piange per far pietà dopo i suoi errori, ma la madonnina ha stancato, è un clone mal riuscito a far danni non in grado di intendere e di volere in quanto teleguidato, e infatti una bomba ligiamente sulla testina gliè arrivata
con educazione, discrezione, tranquillità.
Can anyone PLEASE help me understand the talk? Even a bit of it?
There's specification and then there's implementation now you can implement in any language of your choice so don't worry about it first instead we should think first interms of what and how of our program and that thought can be expressed by specifications and TLA+ uses math like syntax for program specification it gives us a bird's eye view of what is happening and how it's happening
I think I could have done quicksort in terms of iteration. It’s the same as taking an equation that’s true for the principal of mathematical induction and showing it’s equivalent/true for the principal of complete induction. The again I guess most people freeze up when THIS dude is asking.
czcams.com/video/-4Yp3j_jk8Q/video.html - "This is what it looks like in ASCII". Camera shows the slide for 1/10 of a second. Brilliant editing.
Well he is a living legend and I have immense respect for him but seriously didn’t expeted this at 23:10 😂
The bibliography is cited with symbols. Rare.
Page 375
D The Defendant. New York: Dodd, Mead and Co., 1902.
GOAT
8:32 Functions
10:29 limitations of function
The profit is at the margins [56:35] :-)
Is he Steven Spielberg's brother ?
thank you sir for inventing microsoft 😌🙏
he didnt invent microsoft wtf
I find that experience combined with adherence to common design patterns and "best practices" is enough to avoid the types of architectural defects that Leslie believes we need his formal verification for. Formal specification / modeling and verification is a costly additional layer that makes sense in industries where someone may die if your program has a bug and you can afford to spend the additional time and effort, and it's just not worth it in the rest. The bug is usually in the implementation rather than the architecture anyway, down in a layer much below the specification and where static analysis / LINT tools are going to be much more expedient and helpful.
If that xbox360 bug made it to production it could save millions of lives!
42:05 challenge accepted.
He and Jaron are ❤
omg, 55:26 this question is really rude after leslie lamport talk for 50 minutes. but yeah leslie handling this with humble attitude.
15:20 speaks like a mathematician 😂😂
gosh i think he should be a god!! hhahahha, i am just starting to code, and really wanted to learn what algorithms are, by that i confused myself and starting to study logarithms, thinking they were algorithms )))
😂
42
Plus cal 40.20
50:30 "...every thing is a patch" lol
yo, this dude was in breaking bad. he's the junk yard guy.
LMAO
10:47
55:15 "Most programmers don't use formal specifications anymore" said the PhD in response to a talk about why people *should* use formal specifications. Bruh how did you get a PhD? Do you know how to listen to what someone is saying?
Classical activist mentality I suppose. We are tribal entities after all, so his direct challenge is appropriate in the realm of tribalism. But very rude.
Preferable speed 1.5
Thank you.
24:30 did that intern get a job offer
Leslie’s hawt
Yeah he isss
please tell sir pleasee tell about Distributed Deadlock Detection: system model, resource Vs communication deadlocks, deadlock
prevention, avoidance, detection & resolution, centralized dead lock detection, distributed dead lock
detection, path pushing algorithms, edge chasing algorithms. Agreement Protocols: Introduction, System
models, classification of Agreement Problem, Byzantine agreement problem, Consensus problem,
Interactive consistency Problem, Solution to Byzantine Agreement problem, Application of Agreement
problem, Atomic Commit in Distributed Database system
He's come here looking for an explanation for Advanced Operating Systems algorithms lol
The teacher said the domain is 0,1,2,..... and then later he mentioned it as set of Natural numbers. But '0' is not a natural number
Before doubt, you shall at least check.
There is documentation for specifications and not all are think in mathematics.
but problem with that is its in words and its not easily verifiable by a tool. Ofcourse documentation is good for a new human user of the system to get started but when it comes to automated verification by a tool the worded documentation is of no use.
Almighty God is One And Blesses Everyone
There are many gods
☕
Writing requires thinking lol
inventing AI we should think before taking over the world…...
may stop before the sun explodes LOL
function sort(A) {
if (A.length < 2) return;
const U = [[0, A.length - 1]];
do {
const b = U[0][0];
const t = U[0][1];
if (b != t) {
const p = Partitions(A, b, b, t);
U.splice(0, 1);
U.push([b, Math.max(b, p - 1)]);
U.push([Math.min(p + 1, t), t]);
} else U.splice(0, 1);
} while (U.length);
}
function swap(A, b, t) {
const ab = A[b];
A[b] = A[t];
A[t] = ab;
}
function Partitions(A, p, b, t) {
for (let i = b; i < t; i++) if (A[i] < A[t]) swap(A, p, i), p++;
swap(A, p, t);
return p;
}
Being a real-world safety-critical programmer, (with an Applied Math Degree, and a Computer Science Degree), I have quite a few questions, if not outright dismissals of many of his claims.
For instance, he only ever refers to the domain of positive integers!
Most of his statements are provably wrong when referenced to Complex numbers, and risibly incorrect when talking about Tensor fields.
He has plainly NEVER done any risk-taking work in Défense or Aerospace projects.
I have.
He has a ACM A. M. Turing Award. You have?
Dude looks like Frank galager 💀
Consciousness is not a program!
Big reason why I feel Cardano will be so successful.
Man needs some serious shaving 🗿
so he's describing test driven development?
Hell no!!! 52:33 - he almost flips out at the TDD guy :P Poor guy :D
lmao that was savage! Didn't know ol leslie had that in him XD
heh, I should be more careful then!
praoist yup... model driven engineering... model based design...
My side note is that, unit tests should still always be extremely useful for codifying the known lower and upper bounds for some function or behaviour. Perhaps I am describing something outside TDD. I think Leslie is making the point that your initial model specifications help you determine the functions and finite state machines necessary to solve the problem, so TDD is some reality that exists after this is already done, so you can't start there. But he won't be saying you can't still make unit and integration tests that ensure your functions and behaviour are working according to your spec.
dude all the bs comments about how useful this lecture is and how much they learnt, I personally did not find it very useful, but I'm very sure that Leslie Lamport is a top notch individual in his fields of concern, for me as a programmer, specifications has not been all that useful.
Why would you put ads on something like this? What a travesty...
The foamy guilty arguably rush because postage ironically reject modulo a clumsy spade. third, petite curler
No monads and categories here, I‘m out
LOL - a lunatic once said 'the code is the design' ....
This seems like the pseudo code version of Test Driven Development
Yeah but it isn't pseudo code, but actual verification of defined models.
not at all.. it is far from it.. that was the same question by the audience member on specification by example. 10 examples may give a new person on the project a little bit of an idea on what the program is but not the exact specification of it. its like if i give you 10 data points on a sine wave plot would you be able to guess its a sine wave .. its only me who knew it but you will need to spend lot of time deciphering it.
i watched this a long time ago and didnt get it. i rewatched it now and it made more sense. understand the quicksort example fully, it is not a tdd example.
it's using math and logic to define the spec. though to be honest, im not sure if it's all that practical especially in domains where programmers are asking "so it's just tdd, right?" it's more of an addition to the process of creating software. lamport is saying defining the spec is important enough in some cases that we need tools to do it formally.
i have always agreed, and any mathematically minded person would, that tdd is "dumb". we do not define the digits of pi through tdd, it's through math. likewise, tdd may be great when you're not doing hard math. it's a way of building software when the behaviors are trivial.
@@mescellaneous so between not getting it first time and then getting the second , what changed in between ?