Leslie Lamport: Thinking Above the Code

Talk starts at 2:15

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.

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

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

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

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

Amazing Leslie, thank you for sharing it!

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

He's totally right about a spec by example. This is why the majority of coding tutorials end up being not terribly useful.

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

Very well made and super informative.

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

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

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

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

Excellent talk :-)

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.

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