i'm 44 yr old software developer, I thought I was too old. Good to see this.

The approach is incredible… Being fresher and mathematically oriented it’s best to understand the beauty of programming. Thank you for it.

Talk starts at 2:15

One of the best talk , I have ever heard ...... Great !! Thanks !!

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.

Why this great talk is recorded like this? Leslie has very well prepared slides, but we miss most of it.

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

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.

This is something like a gold mine that nobody(at least most) people are missing out on. Mathematical thinking.

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

Amazing Leslie, thank you for sharing it!

Slides: www.microsoft.com/en-us/research/wp-content/uploads/2016/07/leslie_lamport.pdf

Excellent talk. This answered my questions and solved most of my difficulties, Thanks.

Very well made and super informative.

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

"function in math is very different than functions in programming languages..." I used to think so too...but then I met Haskell!

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!

"6 Specs are better to understand than a 800 line code..." This is cool...!!!

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.

Very good talk,. Much of the code out there is like a vortex. Siren code

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.

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

Programming is like the work of a film director when he works on thinking before applying

Excellent talk :-)

amazing explanations.

Is there a link to slides?

Here is the slides PDF www.microsoft.com/en-us/research/wp-content/uploads/2016/07/leslie_lamport.pdf

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

masterpiece thinking!

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

wondering how we can write specs for features of a frontend and backend system

Is this lecture in South Africa?

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

why (0,0) was in ordered pairs, for the square function on Natural numbers ? and he also considered 0 in domain.

He is like Steve Jobs, but with a different shirt.

When I envision a mad scientist. A computer master. I envision Leslie Lamport.

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.

Ty

The scientific problem in natural systems is that the state variables are seldom known. Or, putting it more positively, have to be discovered.

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.

Can I just use your blueprints?

I didn’t understand it but this guy is awesome!!!

Lol when that first guy asked about specification by example I IRL facepalmed

Can anyone PLEASE help me understand the talk? Even a bit of it?

Bookmark: 13:00

thanks a lot. this is super useful to me.

No royal road to math? I think was Gauss?? XD. Amazing and inspiring talk by the way

The bibliography is cited with symbols. Rare. Page 375 D The Defendant. New York: Dodd, Mead and Co., 1902.

1:41 i didnt expect ms would cention latex in its presentations

for thinking we have to writing

I am hooked on TLA+

kzfaq.info/get/bejne/Y5qJo5abxNDPaIU.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 profit is at the margins [56:35] :-)

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.

GOAT

Is he Steven Spielberg's brother ?

42:05 challenge accepted.

If that xbox360 bug made it to production it could save millions of lives!

omg, 55:26 this question is really rude after leslie lamport talk for 50 minutes. but yeah leslie handling this with humble attitude.

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.

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 )))

Plus cal 40.20

thank you sir for inventing microsoft 😌🙏

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?

8:32 Functions 10:29 limitations of function

42

10:47

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.

Preferable speed 1.5

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

yo, this dude was in breaking bad. he's the junk yard guy.

He's the guy who gave us confortable condoms, right?

15:20 speaks like a mathematician 😂😂

50:30 "...every thing is a patch" lol

He and Jaron are ❤

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

Leslie’s hawt

24:30 did that intern get a job offer

There is documentation for specifications and not all are think in mathematics.

Why would you put ads on something like this? What a travesty...

Almighty God is One And Blesses Everyone

☕

inventing AI we should think before taking over the world…...

may stop before the sun explodes LOL

Writing requires thinking lol

Man needs some serious shaving 🗿

Consciousness is not a program!

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 looks like Frank galager 💀

so he's describing test driven development?

This seems like the pseudo code version of Test Driven Development

LOL - a lunatic once said 'the code is the design' ....

No monads and categories here, I‘m out

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.

The foamy guilty arguably rush because postage ironically reject modulo a clumsy spade. third, petite curler

"If you are thinking without writing you are only pretending to think." So i guess Stephen Hawking is just pretending then. :)

he is very sensitive old yunk yard recicler