Leslie Lamport: Thinking for Programmers [video]

http://channel9.msdn.com/Events/Build/2014/3-642

by mfn • 12 years ago

133 32 12 years ago

channel9.msdn.com

hatred• 12 years ago

Is anyone else having issues seeking across the video i.e. moving to a particular time in it ?

dredmorbius• 12 years ago

Download and view it locally with the player of your choice: mplayer, xine, vlc, etc.

I can seek fine in mplayer.

brianmwaters_hn3• 12 years ago

The video won't play at all in my browser. FF24 on Gentoo.

dethstar• 12 years ago

You need silverlight.

gabriel• 12 years ago

The site offers alternative downloads of the video file. You should be able to watch these videos on linux with vlc or one of your favorite video players.

pedalpete• 12 years ago

I've found the streaming of anything from build to be completely unreliable from the channel9 site. You can download the vids, but the download times are also horrendous. Seems to me this would be a great excuse for a company to use a torrent to spread their content. It's free anyway, why not use it and promote the legal use of a great technology?

brianmwaters_hn3• 12 years ago

I think the way they choose to introduce him in the blurb below the video is funny: "inventor of Paxos and developer of LaTeX." But Leslie Lamport has a Turing Award!

teraflop• 12 years ago

The blurb might well have been written before he got that award.

brianmwaters_hn3• 12 years ago

That's true, I think he just got it, even though the award is for 2013.

marshray4• 12 years ago

Everybody knows Lamport, LaTex, and/or Paxos.

But I don't think I could name the organization that gives out these so-called 'Turing Awards' or any other recipients.

Aqueous• 12 years ago

The Turing Award is a fairly significant award, as awards go. It's kind of like the Fields Medal or the Nobel. So it means enough to make Lamport getting it a big deal.

mbrubeck2• 12 years ago

Since ACM is the major organization for computer science research, nearly everyone who has studied Paxos should know of the ACM. Lamport's own seminal papers introducing distributed clocks and Paxos were published in the journals Communications of the ACM and ACM Transactions on Computer Systems, respectively.

jeffreyrogers• 12 years ago

I've read a number of papers recently discussing various software design techniques for improving the ease with which bug-free code can be reduced. Most of these papers are infeasible in practice because they rely on new language features that aren't found in any mainstream language. For example, the paper "Out of the Tar Pit" suggests "Functional Relational Programming" as a method of reducing complexity in software. Unfortunately, I can't evaluate the efficacy of FRP in practice because there is no language allowing for it, and even if there were, it wouldn't be a language anyone would use since there would be no support for it.

In contrast to those approaches, Lamport's ideas seem quite reasonable and have the benefit of being language agnostic. He definitely has a lot of interesting ideas here!

tel2• 12 years ago

FRP is implemented in Haskell, Scala, Java, C#, and JavaScript off the top of my head.

jamii• 12 years ago

I suspect you are confusing Functional Relational Programming with Functional Reactive Programming. The latter revolves around programming with time-varying streams of values and has been implemented many times. There is an interesting discussion of related problems at http://lambda-the-ultimate.org/node/4900#comment-78949.

Functional Relational Programming is defined by using relational constructs to model data and manage change and using pure functions to express computation. The only serious implementation I'm aware of is http://boom.cs.berkeley.edu/

dragonwriter• 12 years ago

For example, the paper "Out of the Tar Pit" suggests "Functional Relational Programming" as a method of reducing complexity in software. Unfortunately, I can't evaluate the efficacy of FRP in practice because there is no language allowing for it

Are you sure?

http://clojure.com/blog/2012/02/03/functional-relational-pro...

eurekin2• 12 years ago

This is very interesting - I'm eager to start using it... Does anyone know a quick way to start in a business domain?

At my job, I maintain a well established (read: old) product for moving money. There are a lot of business rules. Formal specification for it all is out of question.

There are though, certain well encapsulated modules which play only a support role -- there is a very faint connection to the core domain, which in this case could easily ignored. One module is a version of "personal task management".

Let's say, the personal task management domain is just being specified. Normally, we'd write in the spec:

* any user has a list of tasks

* any task can have a number of steps

* any step can be started or finished

* user can mark any step as finished or started

* if all steps are finished, the task is closed.

Can anyone help me in expressing these kind of rules in the TLA, please? How could the TLA spec be useful for me?

I find it very interesting to play with, because those "supportive domains" in our product tend to grow quickly and more often than not there comes a change request such as this one:

* the step can have a type (other words: there are two kinds of steps now): manual and automatic.

* all "old" steps are manual steps

* the automatic step is being managed by the application (user cannot change whether it's finished or started)

* the automatic step is executed by some external actor, let's say a process running once a month.

Now, does TLA allow me to "grow the spec" as the requirements come in? Does anyone has this real world, business experience with it (or any other formal specification method) and found it really useful? The example Leslie gave in it's talk (XBox memory bug) seems to be found only by the careful thinking phase and not by TLA directly. Other examples where sorting and finding GCD...

I have no idea how to start using it in my domain. Anyone has the experience (not necessarily with TLA/PlusCalc)?

--- Update

I thought a little bit more to make it closer to what kind of problems we are facing (it's still fictional, so it might not be too coherent).

There comes another change request - the client demands more security! A rule is added:

* any step within the task can be executed only by the same user which added the task to the system.

Now, we have a problem! Automatic processes run with a fake user id ("batch_user_001") and cannot finish the required steps. The user also cannot, since the step is automatic one.

What could we do now? OK, first possibility to explore: use the roles and delegation. Maybe the user should have a role the same as the process? Now the rule could be:

* any step withing the task can be executed only by the user with a role the same as the user adding the task.

Yeah, the tasks can now be processed. OK, but is this the best solution or more of a workaround?

Maybe the process shouldn't run with any user id at all? If I change this part of system how can I check if something else breaks? Like the GUI which assumes "there always IS a user id".

Enough with the fictional scenario. Some conclusions follow.

I believe the formal spec is exactly the tool which would allow to test the interactions of changes more quickly than guessing and/or relying on the expert knowledge (maybe on a sick leave). I be it must be used exactly for the purpose! I considered finding it on my own, but maybe someone here already does it. If yes, kindly please speak up about your experience. :)

crazygringo• 12 years ago

Can anyone provide a TL;DW? The video's an hour long, without any kind of transcription, and there are only 4 slides which don't explain anything...

eurekin2• 12 years ago

At the beginning, Leslie explains why specification is important. He gave few convincing (me) examples and then introduced the idea of formal specifications.

The formal specification allows you to find design bugs, before writing any code. An anecdote about XBox memory model is given: a certain hardware bug (in the memory unit) once made it's way into production would stop any XBox after 4 hours of using it. The bug wouldn't be found using any methods the hardware manufacturer was using.

The bug was found due to an engineer who was formally specifying the memory model. He provided a bug description and the response was: "Invalid, the system cannot come into this state". The engineer than responded with a scenario leading to the state using the rules which governed the memory model. Eventually the bug was fixed.

Leslie moved to more down to earth examples: finding greatest common divisor (Euclid's algorithm) and QuickSort. They were expressed in pseudocode and with minor adjustments as a TLA spec.

In all examples the same conclusion was given: having written only the code it would be very difficult to find the design bugs.

acqq• 12 years ago

The languages Lamport uses:

http://research.microsoft.com/en-us/um/people/lamport/tla/tl...

http://research.microsoft.com/en-us/um/people/lamport/tla/c-...

ismyrnow• 12 years ago

Although he talks a bit about formal specifications and tools for writing and verifying them, his talk has a few really great parts about informal specs.

I'd recommend watching 23:22-30:42, where he gives an example of where an exhaustive semi-formal spec was critical for writing good code.

I'd also recommend 44:00-54:00, which I think is the most broadly applicable part of the talk, where he discusses the need for thinking as writing, and writing specs before coding.

hibikir• 12 years ago

I wish he talked about specification's real problem.

There are many ways out there to write specifications. Some are good, some are bad. Let's assume we got a very good one. Then let's say I actually implement the specification correctly. So now I have a program and a spec it matches.

But then comes the problem: My application needs to change. Along with it, we need to change the specifications. If said specifications are too high level, then we start changing code without changing spec, and it doesn't take long before the spec is a dead document. If the spec is too low level, then change is hard, because the specification's friction becomes unbearable quickly.

So the problem quickly becomes the fact that writing specifications isn't really any easier than writing the code. It's the same problem that plagues many testing suites in practice: They either test too little, or test so much they increase the cost of development way past their value.

I am not saying we should not write tests, or specs. But what I really want to know is how to write a good spec, or a good test suite, because if those are bad quality, they actually become detrimental. At work, I just spent a solid two weeks trying to fix extremely overspecified tests: Hundreds of them that should have never been affected by the code changes. The people that write such tests will probably write terrible specifications that are just as brittle.

So don't show me a new specification language: Show me how said language makes it easy to write good specifications, and hard to write bad ones.

auggierose• 12 years ago

If you cannot write good specifications, then probably you shouldn't, except for exercise purposes. There are then two possibilities: 1) you work in a team where there is a job for someone just implementing specs instead of coming up with good ones (usually such a team is mediocre at best) 2) you should be fired and replaced by someone who can write good specs.

grogers• 12 years ago

Writing a formal specification using something like TLA+ is actually very much like writing unit tests. Therefore, many of the same problems apply. The main difference is that you are testing your design, not the implementation. You are trying to work at a much higher level than the actual code.

That's why it is most useful for checking concurrency. It is hard for humans to mentally think about all possible interleavings of events, hard for fuzz testing to catch rare interleavings, but very easy for a computer to check all possibilities with breadth-first search.

By no means are specifications a complete answer, even making sure your implementation implements the spec is hard. But it is another useful tool in the arsenal.

vinodkd• 12 years ago

My favorite bits from the video:

- Why should you think? Because it helps you do things.

- When should you think? Before you write any code.

- How should you think? By writing. "Writing is nature's way of letting you know how sloppy your thinking is". To think, you have to write. If you think without writing, you only think you're thinking.

- What to write? Write a specification. It can be simple or "mathematical prose" or a fully formal specification. A spec is simply whatever you write before coding.

- (00:44) Why write the spec? To be sure what the code should do before you write it.

- What code should you specify? Any code that someone else might use or modify. That someone could be future you.

He did talk about his TLA+ tool, but the points above were the thrust of this talk.

Leslie Lamport: Thinking for Programmers [video]

Related Stories