Lamport TLA+ Course Lecture 1: Introduction to TLA+ (HD)

Рет қаралды 40,060

Күн бұрын

IMPORTANT NOTE!: This is a mirror of Lamport's TLA+ lecture videos with some chapter markers in the video description from Lamport's site for ease of viewing on mobile devices, or other platforms and connection setups where KZfaq is the most optimal "format". For the original files, resources, errata, and more, please visit lamport.azurewebsites.net/vide... or the original page which is linked below.
Original Description: Explains what TLA+ is and why you might want to use it. It introduces the concept of a state machine.
Original Link: lamport.azurewebsites.net/vide...
Corrections: lamport.azurewebsites.net/vide...
Contents
0:00 - Intro
00:05 - Prologue
00:46 - What is TLA+?
02:46 - Abstraction
05:08 - What Engineers Say
09:41 - What Can TLA+ Check?
10:37 - The Basic Abstraction
12:50 - State Machines
14:25 - A Tiny Example
19:50 - Epilogue

Пікірлер: 35

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

@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

@julissadc6303 Күн бұрын

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

@vapourmile 3 жыл бұрын

I'm only as far as 17:15 but this is very interesting. Really valuable. It's interesting how Leslie's experience with formal specification really shines through as most of this talk is a series of very precise statements.

@Bill82078 4 жыл бұрын

very special sense of humor :)

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

@charlessmyth 2 жыл бұрын

Discovered this via a 2014 Microsoft talk :-)

@goodboy9758 Жыл бұрын

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

@veramentegina 5 жыл бұрын

Thank you!! Can't wait to start using TLA+. I definitely need this.

@JibletParade 2 жыл бұрын

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

@vibhatha 4 жыл бұрын

Very interesting !!! Re-thinking engineering.

@imimran924 Жыл бұрын

thank you sir

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

@letme4u Жыл бұрын

congratulations for making to Linux foundation.

@srebrnimedved 4 жыл бұрын

Vrh ✊

@kyuantym Жыл бұрын

Prof Lamport

@trejohnson7677 3 жыл бұрын

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

@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

@TatianaRacheva 8 ай бұрын

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

@arslanrozyjumayev8484 Жыл бұрын

i belong here

@Dolshansky 6 жыл бұрын

This is all extremely interesting, but I'm afraid it might cause a new team to overengineer a pre-product architecture. This seems to be applicable at large waterfall corporations that are ready to rearchitect an existing system using all the lessons they learnt from the first one.

@baganatube 5 жыл бұрын

People over-engineer all the time, with every existing programming language or modeling tool. So it's not a problem in the tools, it's a problem in the engineers, likely due to lack of experience (luckily, that's something that can be earned eventually). If you think a system is likely to be over-engineered *because of* the use of TLA+, that system might probably fall into the "TLA+ is not useful" category mentioned by the professor. This tool is designed mainly to model complex distributed systems, where few people can turn their heads around just by thinking. At least I'm having this problem - my brain is just too primitive to intuitively conclude that my distributed system will work as expected in every possible concurrent execution, especially on failures. I'm hoping TLA+ would help me on that.

@user-rg6qw2mi1d 5 жыл бұрын

@@baganatube : what industry are you in?

@kellymoses8566 3 жыл бұрын

Software is riddled with bugs and wider use of TLA+ would be a huge improvement.

@Kenbomp 3 жыл бұрын

It depends there's over engineering and there's improving. The falacy of coding is coding. There alot of thought but people don't see it. It doesn't show up on GitHub. They should have used it on cyberpunk 2077. Anything that reduces code is a good thing.

@pino6782 3 жыл бұрын

If I understand correctly the purpose of this tool, I think it does not force you to overengineer anything. You have a model how your (future) concurrent system should behave, and you use TLA+ to check what the points of failure are, if any. You may decide to fix or not to fix those. How you fix them, it's up to you, TLA+ will not dictate that. I think "overengineering" the system is something that people do (models may already be overengineered or fixes to issues TLA+ finds can be overengineered), TLA+ merely explores the paths of execution and tells us what may go wrong where.