TLA+ Video Course

Пікірлер

@julissadc6303 4 күн бұрын

I like that he kept changing clothes to kept the viewer engaged

@Vatsal-rq2sw 25 күн бұрын

why if condition is expressed as and operator and not by implies operator ?

@Datamining101 Ай бұрын

"Laytek, or lahtek if you prefer" well now we know how to say it 😂

@viewerontube 3 ай бұрын

Good old school... Pretty clear and laconic. Thank You Leslie!

@xiongxin8802 6 ай бұрын

Thank you for your course, you are one of the coolest professors I've ever seen.

@user-ds1pu2vc8s 7 ай бұрын

It's all fun and games until this lecture..

@TatianaRacheva 8 ай бұрын

Tip on reading the AWS paper: skip the first 1.5 pages. They should have shortened the intro to 1 sentence.

@andrewhzy7372 9 ай бұрын

don'e know wahere to find the spec code, when he says copy and past the spec code from the web page, can anyone share with me the web page?

@YoussifSalama 9 ай бұрын

You have to visit the original website it’s uploaded too. It’ll then pop under the video when he mentions it

@bwandesky Жыл бұрын

Learning TLA+ opened my mind to a different way of thinking.

@aminsetayesh5429 Жыл бұрын

This course was amazing. Thank you!

@sidekick3rida Жыл бұрын

1:19 the language was SPIN. Here's the quote… "While we had an initial bias toward using SPIN [7], in the end it was decided to use TLA/TLC from Leslie Lamport. [2] Although the mathematical notation of the TLA language was first considered a hindrance versus the C-like Promela language of SPIN. In the end this has proven to be a major benefit as it forced to reason in a much more abstract way about the RTOS."

@EvgeniyDolzhenko 5 ай бұрын

haha, thank you :)

@fernandoquinonez5040 Жыл бұрын

Cost me few minutes to understand why use 'and'

@fernandoquinonez5040 Жыл бұрын

Nice

@kyuantym Жыл бұрын

MR Lamport is an inspiration

@letme4u Жыл бұрын

congratulations for making to Linux foundation.

@kyuantym Жыл бұрын

Prof Lamport

@stevekimani9578 Жыл бұрын

imagine if this man filmed all this video in one day this means that he had to change clothes in every slide, if so (deterministic 😉) it means he is a psychopath. I just wanted to watch the introduction but he go me hooked.

@VidhathShetty Жыл бұрын

I'm amazed as to how even experienced cs people have ignored this in their workflow. Even with my self ( a beginner). This cuts down so much of the learning curve thank you Mr.Lamport for your contribution 🙏🙏

@imimran924 Жыл бұрын

thank you sir

@raoulhatterer957 Жыл бұрын

I wonder At kzfaq.info/get/bejne/arSke7iXvdLKZJs.html you define Pick and Add1 starting with an \/ In your previous video kzfaq.info/get/bejne/atmeqr2dnJiak2g.html you didn't do this which seems more logical to me because the definition of "Next" includes the \/

@goodboy9758 Жыл бұрын

More defi protocols need to start using this, perhaps even should hire dedicated formal verification engineers for sc development

@tubex1300 Жыл бұрын

Prof thanks for this great vids I love them the most

@juandomandl3282 Жыл бұрын

This is awesome.

@arslanrozyjumayev8484 Жыл бұрын

i belong here

@leilu5301 2 жыл бұрын

If '=' means equality in Next, then when will i' and pc' be updated?

@atikzimmerman 2 жыл бұрын

The fact that there are x2 views to the previous lecture makes me feel better (several of that views are mine)

@handsanitizer2457 2 жыл бұрын

Gangsta gangsta

@warwolt 2 жыл бұрын

I'm not sure this is 100% correct, but I think that the syntax [rmState EXCEPT ![r]="prepared"] uses the bang just as a shorthand for the name in position of rmState. You can also write [rmState EXCEPT !.r = "prepared"], so the bang just gets you out of having to write "rmState" twice.

@borincod 2 жыл бұрын

He had to add at the last minute: "Now, stop the video and watch Die Hard 3 !"

@verfran 2 жыл бұрын

You got me thinking.....

@ZergRadio 2 жыл бұрын

I have never understood how smart people (or at least the people recording the video or someone reuploading.) have such low quality audio (It is so annoying.) I was on another side on "gentle introduction to TLA+" It was all text. Problem was it was low quality video so I could not see the smuggy text. (Some of us are old.)

@lam7572 2 жыл бұрын

leslie lamport is goat 👍👍👍👍

@charlessmyth 2 жыл бұрын

Got all of that downloaded and running on my Debian Bullseye :-)

@charlessmyth 2 жыл бұрын

That was good :-)

@nervous711 2 жыл бұрын

7:57 Was the lowercase rm in square bracket meant to be r that specified on the right side of rmState?

@atikzimmerman 2 жыл бұрын

I would say that r has a declaration scope inside it's square brackets, and rm (which is not formally declared though) is outside of it, so you have to have a different variable.

@charlessmyth 2 жыл бұрын

Discovered this via a 2014 Microsoft talk :-)

@JibletParade 2 жыл бұрын

I need a state machine representing the possible next values of hat

@tariq3erwa 2 жыл бұрын

Ive always wondered about the boundaries between programming and mathematical thinking, this gives me a satisfying answer, thank you. And nice costumes! :)

@ArquimedesOfficial 2 жыл бұрын

At least you have the right reasoning, some ppl thinks code writing its programming, and programming it’s an art form, omg lol.

@TrueDetectivePikachu 2 жыл бұрын

Why Google group tho? Why not Discord or reddit?

@handsanitizer2457 2 жыл бұрын

This was 5 to 4 years ago, people used to use those still

@conduit242 2 жыл бұрын

Lamport is definitely flying a buckling spring keyboard 💯

2 жыл бұрын

Thank you for this video. I'm curious about the different solutions when the invariant big /= 4 is chosen. You showed big = 4 and small = 3 in the end. In another run I found (sadly only) one error with big = 4 and small = 0 in the end. It is always just one error found. Does it stop at the first invariant found? How can we find any errors leading to this big /= 4 at the end?

@twodirectionalfoil 2 жыл бұрын

"stop the video and convince yourself" 😆

@MrEtronic 2 жыл бұрын

dont want to flex but i made the most popular distributed consensus algorithm and won a turing award for it ... ok DOC we get it you are the GOAT

@conduit242 2 жыл бұрын

THE. GOAT.

@trejohnson7677 3 жыл бұрын

Well atleast I don’t have to do this too, now I can focus on my emacs config!

@ytdlgandalf 3 жыл бұрын

Okay what just happened.. I could follow along pretty nicely till this lecture.

@ytdlgandalf 3 жыл бұрын

this pace is so awesome. Why wasn't my University experience like this.

@ytdlgandalf 3 жыл бұрын

this is worth so much, pity we as a industry do so little with it. seriously.. this is the stuff that will make us real engineers, instead of code ejaculators.

@joanjett69697 Жыл бұрын

'code ejaculators' is the funniest, best phrase i've heard to describe MYSELF in a long time

@droneborg19 Жыл бұрын

Why is it not used? Because of time/schedule pressure?

@keithteo9007 Жыл бұрын

"Code ejaculators" Im saving that one for later use

@clothes5049 Жыл бұрын

@@droneborg19 This is late, but my assumption is that time limitations, low perceived value by managing entities, and lack of software engineers that actually are familiar with formal methods all contribute to it.

@stultuses Жыл бұрын

@@droneborg19 I think it is also because we have traditionally not needed to scale solutions up to truly global scale So we have things that for now are 'good enough', good because over time we have hashed out patterns that we now know have issues, enough to avoid them As we move to the next scale up, issues are going to creep out of the woodwork. TLA+ with it's rigor on proofs, would eliminate the trial by error (and improve) methodologies we are currently using

@kellymoses8566 3 жыл бұрын

This dude is, like, really smart.

@sefirotsama 2 жыл бұрын

He won a turing award and invented... way too many things for just a comment on youtube

@huailinchen 3 жыл бұрын

I cannot help laughing when watching to the end. So cute, Dr. Lamport. We all love you!

@daviskipchirchir1357 2 жыл бұрын

with the natural background he uses I almost feel like I am being let into the fundamental secrets of programming

Ең жақсы KZfaq

Пікірлер