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).
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.
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
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.
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.
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.
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!
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
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
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.
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
@ 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.
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)!
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
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.
*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.*
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.
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.
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
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
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.
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 )))
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.
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.
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.
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.
how do we know ‘writing’ wasn’t invented when man was hunting the sabre tooth tiger? we can say ‘writing’ as we know it today wasn’t invented but that’s not to say man did not ‘plan’ ahead of time using some set of well understood symbology. therefore, bad example.
03:31 "Writing is nature's way of letting you know how sloppy your thinking is. To think, you have to write. If you're thinking without writing, you only think you're thinking." 06:44 "Well, writing requires thinking." So does thinking require writing or does writing require thinking?! I suggest that mr. mathematician gets his sloppy logic right on this one (and others), since by these statements, one cannot either think or write because each of them requires the other, ad infinitum. A bit of a which was the first, chicken or the egg problem, albeit that one does actually have a solution, if the egg was a dinosaur one in the first place, like findings seem to indicate as well. Also, he should stick to his theoretical math that others can apply in practice and avoid rating how people think or give lessons on the differences between coding and programming to actual coders / programmers, because he obviously doesn't understand either. Other than that, probably a nice and above average fellow, even though as it's customary in the world, inventors never earn at the level of CEOs, if they earn something, that is. Maybe this could be a problem mr. mathematician can dissect better, eh?
Writing coherently requires thinking (about what you're going to write). Thinking doesn't literally require writing, but writing down your thoughts motivates you to think more carefully about issues that you may have hand-waved away in your mind.
@@Raging.Geekazoid Indeed - writing down the thought process makes it clearer and is naturally more suited for complex issues, where it can spur further thinking on the subject. My problem with what he said is the downright absurd idea that thinking requires writing. That kind of suggest that if a person isn't activating in a field like his where things have to be written down due to the inherent complexity of the process, then that person isn't thinking at all or just halucinates that is thinking - in other words, the person is stupid. I know I'm probably overthinking this (and I didn't even have to write it, by the way), but it certainly looks like a veiled reference to that. In other videos he also suggests that a programmer must somehow be a mathematician first (just like he is, obviously), because otherwise the code / program would not be "up to standard", not to mention insisting on the apparently critical differences between programming and coding (i.e. he's programming, while the rest of the lot are "just" coding). These things, coupled with the idea that thinking requires writing (because it does for him in his projects), emphasize the above suggestion even more. In short, while I agree that nowadays education in general (and not only in the US) is not what it should be and many people have gaps in knowledge as a result, it's a bit disrespectful - and inaccurate as well - to both contemporary people and to our ancestors to suggest that they don't or didn't think just because they didn't have a piece of paper or similar to write down the result. Thinking is not a particularity exclusive to folks activating in a certain scientific field, let alone a particularity of humans if we're at it - they don't have a monopoly over it. Only the complexity of the subject is.
@@yincognito You're taking what he said too literally. Human beings have evolved a strong tendency to focus on the most important aspects of things and forget about the details, and that approach just doesn't work in software development and other STEM fields. So, from a practical standpoint, very few people in this world are able to think clearly and precisely without the regimentation of writing down their thoughts. Lamport doesn't mean to offend, he's not making veiled references to anything. He's just explaining the facts of human nature as they're widely understood by experienced professionals in the software business. Writing down plans is also common in other fields, and there may be special reasons (e.g. secrecy and the general messiness of the social world) for not recording everything.
@@Raging.Geekazoid Well, you're right and I already hinted at that in my earlier reply when I said that complexity is determining whether thoughts must be written on something or not, like it happens in STEM fields. He probably didn't mean to offend or make references consciously, since he doesn't seem to be that kind of person ... though he could have put more thought (pun intended) into formulating what he meant so that it couldn't have been misunderstood and be logically accurate (since he's a mathematician in the first place). After all, I'm not the only one seeing between the lines or disagreeing with some of his statements, there's at least one in the audience and some in the comments as well. Other than that, I don't have an issue with the guy or what he talks about. He seems like an outsider to the commercial and business part of the environment, and that is a good thing. I guess I just expected that for a person working on correctness, reliability and otherwise precision related things in the computer area to be just as precise in expressing what he means in words. But then, who knows? Maybe he didn't pay much attention to it, or like most mathematicians, he's better with numbers than words.
@@jessepowellr4 Think again. The ad populum argument is a fallacy in cases where it's the ONLY one used to support a conclusion, which is not the case here. I had already exhausted a bunch of other independent and logical arguments before using the ad populum one to supplement the previous ones. If one already proves that water boils at 100 C at sea level pressure and then mentions that others noticed the same thing in order to emphasize it, that is by no means an invalid conclusion, quite the contrary. Also, as a side note, the ad populum fallacy is used in all democracies around the world to govern us and tell us what's "right" or "wrong" based on the majority's opinions (or votes, in this case), so maybe you'd want to question that aspect as well, since we're at it. Not sure if you'd be able to do that though, judging from your earlier reply...
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
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)
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.
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
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.
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.
One of the best talk , I have ever heard ...... Great !! Thanks !!
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?
Slides: www.microsoft.com/en-us/research/wp-content/uploads/2016/07/leslie_lamport.pdf
Thank you
Thanks!
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.
Yea! I'm getting frustrated at this point!
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?
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.
He's math guy not coding language guy😂
Excellent talk. This answered my questions and solved most of my difficulties, Thanks.
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
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 👆
"function in math is very different than functions in programming languages..." I used to think so too...but then I met Haskell!
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.
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
@ 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
Amazing Leslie, thank you for sharing it!
I've studied your clock algorithm in distributed systems
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)!
"6 Specs are better to understand than a 800 line code..." This is cool...!!!
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
Programming is like the work of a film director when he works on thinking before applying
Very good talk,. Much of the code out there is like a vortex. Siren code
Check out 56:18 this could be a strong motivation for some people to use formal spec.
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.
When I envision a mad scientist. A computer master. I envision Leslie Lamport.
Excelente approach clarisima
*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.😊
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.
amazing explanations.
Very well made and super informative.
The scientific problem in natural systems is that the state variables are seldom known. Or, putting it more positively, have to be discovered.
Is there a link to slides?
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.
Can I just use your blueprints?
omg, 55:26 this question is really rude after leslie lamport talk for 50 minutes. but yeah leslie handling this with humble attitude.
Excellent talk :-)
Well he is a living legend and I have immense respect for him but seriously didn’t expeted this at 23:10 😂
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.
Bookmark: 13:00
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
I didn’t understand it but this guy is awesome!!!
1:41 i didnt expect ms would cention latex in its presentations
The bibliography is cited with symbols. Rare.
Page 375
D The Defendant. New York: Dodd, Mead and Co., 1902.
Lol when that first guy asked about specification by example I IRL facepalmed
masterpiece thinking!
Thank you sir
thank you sir for inventing microsoft 😌🙏
he didnt invent microsoft wtf
No royal road to math? I think was Gauss?? XD. Amazing and inspiring talk by the way
I think Euclid
Ty
Is he Steven Spielberg's brother ?
If that xbox360 bug made it to production it could save millions of lives!
for thinking we have to writing
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à.
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.
8:32 Functions
10:29 limitations of function
He is like Steve Jobs, but with a different shirt.
He's the guy who gave us confortable condoms, right?
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 profit is at the margins [56:35] :-)
Is this lecture in South Africa?
thanks a lot. this is super useful to me.
how dare you impersonate me!
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.
ua-cam.com/video/-4Yp3j_jk8Q/v-deo.html - "This is what it looks like in ASCII". Camera shows the slide for 1/10 of a second. Brilliant editing.
What a legend.
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 )))
😂
I am hooked on TLA+
Why would you put ads on something like this? What a travesty...
15:20 speaks like a mathematician 😂😂
42:05 challenge accepted.
24:30 did that intern get a job offer
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.
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?
Honestly i don't fully understand what he's trying to convey
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.
Almighty God is One And Blesses Everyone
There are many gods
He and Jaron are ❤
yo, this dude was in breaking bad. he's the junk yard guy.
LMAO
10:47
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.
GOAT
Kouini transistors
Preferable speed 1.5
Thank you.
Plus cal 40.20
how do we know ‘writing’ wasn’t invented when man was hunting the sabre tooth tiger? we can say ‘writing’ as we know it today wasn’t invented but that’s not to say man did not ‘plan’ ahead of time using some set of well understood symbology. therefore, bad example.
They were called runes
BPlease
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;
}
Consciousness is not a program!
42
03:31 "Writing is nature's way of letting you know how sloppy your thinking is. To think, you have to write. If you're thinking without writing, you only think you're thinking."
06:44 "Well, writing requires thinking."
So does thinking require writing or does writing require thinking?! I suggest that mr. mathematician gets his sloppy logic right on this one (and others), since by these statements, one cannot either think or write because each of them requires the other, ad infinitum. A bit of a which was the first, chicken or the egg problem, albeit that one does actually have a solution, if the egg was a dinosaur one in the first place, like findings seem to indicate as well. Also, he should stick to his theoretical math that others can apply in practice and avoid rating how people think or give lessons on the differences between coding and programming to actual coders / programmers, because he obviously doesn't understand either. Other than that, probably a nice and above average fellow, even though as it's customary in the world, inventors never earn at the level of CEOs, if they earn something, that is. Maybe this could be a problem mr. mathematician can dissect better, eh?
Writing coherently requires thinking (about what you're going to write). Thinking doesn't literally require writing, but writing down your thoughts motivates you to think more carefully about issues that you may have hand-waved away in your mind.
@@Raging.Geekazoid Indeed - writing down the thought process makes it clearer and is naturally more suited for complex issues, where it can spur further thinking on the subject. My problem with what he said is the downright absurd idea that thinking requires writing. That kind of suggest that if a person isn't activating in a field like his where things have to be written down due to the inherent complexity of the process, then that person isn't thinking at all or just halucinates that is thinking - in other words, the person is stupid.
I know I'm probably overthinking this (and I didn't even have to write it, by the way), but it certainly looks like a veiled reference to that. In other videos he also suggests that a programmer must somehow be a mathematician first (just like he is, obviously), because otherwise the code / program would not be "up to standard", not to mention insisting on the apparently critical differences between programming and coding (i.e. he's programming, while the rest of the lot are "just" coding). These things, coupled with the idea that thinking requires writing (because it does for him in his projects), emphasize the above suggestion even more.
In short, while I agree that nowadays education in general (and not only in the US) is not what it should be and many people have gaps in knowledge as a result, it's a bit disrespectful - and inaccurate as well - to both contemporary people and to our ancestors to suggest that they don't or didn't think just because they didn't have a piece of paper or similar to write down the result. Thinking is not a particularity exclusive to folks activating in a certain scientific field, let alone a particularity of humans if we're at it - they don't have a monopoly over it. Only the complexity of the subject is.
@@yincognito You're taking what he said too literally. Human beings have evolved a strong tendency to focus on the most important aspects of things and forget about the details, and that approach just doesn't work in software development and other STEM fields. So, from a practical standpoint, very few people in this world are able to think clearly and precisely without the regimentation of writing down their thoughts.
Lamport doesn't mean to offend, he's not making veiled references to anything. He's just explaining the facts of human nature as they're widely understood by experienced professionals in the software business. Writing down plans is also common in other fields, and there may be special reasons (e.g. secrecy and the general messiness of the social world) for not recording everything.
@@Raging.Geekazoid Well, you're right and I already hinted at that in my earlier reply when I said that complexity is determining whether thoughts must be written on something or not, like it happens in STEM fields. He probably didn't mean to offend or make references consciously, since he doesn't seem to be that kind of person ... though he could have put more thought (pun intended) into formulating what he meant so that it couldn't have been misunderstood and be logically accurate (since he's a mathematician in the first place). After all, I'm not the only one seeing between the lines or disagreeing with some of his statements, there's at least one in the audience and some in the comments as well.
Other than that, I don't have an issue with the guy or what he talks about. He seems like an outsider to the commercial and business part of the environment, and that is a good thing. I guess I just expected that for a person working on correctness, reliability and otherwise precision related things in the computer area to be just as precise in expressing what he means in words. But then, who knows? Maybe he didn't pay much attention to it, or like most mathematicians, he's better with numbers than words.
@@jessepowellr4 Think again. The ad populum argument is a fallacy in cases where it's the ONLY one used to support a conclusion, which is not the case here. I had already exhausted a bunch of other independent and logical arguments before using the ad populum one to supplement the previous ones. If one already proves that water boils at 100 C at sea level pressure and then mentions that others noticed the same thing in order to emphasize it, that is by no means an invalid conclusion, quite the contrary. Also, as a side note, the ad populum fallacy is used in all democracies around the world to govern us and tell us what's "right" or "wrong" based on the majority's opinions (or votes, in this case), so maybe you'd want to question that aspect as well, since we're at it. Not sure if you'd be able to do that though, judging from your earlier reply...
No monads and categories here, I‘m out
may stop before the sun explodes LOL
Man needs some serious shaving 🗿
inventing AI we should think before taking over the world…...
i really wish that software professionals would stop pretend that software and buildings and architecture is related in any way, it is not. just stop
Yep like try to refactor that bathroom and move the kitchen sink to the living room temporarily while iteratively improving the architecture.
Yeah, thank god programmers don't design buildings.
Big reason why I feel Cardano will be so successful.