Leslie Lamport: Thinking for Programmers [video]

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.

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.

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!

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!

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

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

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