Lambda the Ultimate

non-systems/non-critical programming mostly done by app developers

Few popular "apps" run in isolation. They typically comprise client code, server code, and sometimes networks of other devices running the same app (or other kinds of network).

Apps are very often critically entailed in user privacy.

Apps may be critical in a wide variety of other ways. For example, apps that encourage real-world interactions among users (scab cab apps, hook-up apps) can be critical with respect to users' physical safety. Apps may perform financial transactions on behalf of users. Apps may be offering health advice. Apps may become critical communication channels whose unexpected unavailability may be costly. Apps may subtly impair the functioning of the critical devices on which they run.

I could go on but you get the gist.

Silicon Valley elites seem to have made some collective decision, somewhere in the last 10 years, that quality and safety, unintended consequences, and social impact are really unimportant topics. After all it's just apps.

mostly done by app developers with little to no formal education in mathematics or computer science.

Do you mean that they are compliant; short on critical thinking skills; easily manipulated by relatively small sums of money and sketch monetary promises; unprofessional and insecure (thus easy to subordinate) in professional settings; credulous and loyal to any fat-cats who will give them a collective pat on the head; far too easily self impressed; and living in a bubble?

It's OK, though, because although the fat-cats assert out of one side of their mouth that mobile and apps will displace all personal computing and reform the economy and the way they live --- they do indeed say out the other side of their mouth that "what does it matter? geeze, it's just apps!"

p.s.: as I write this the link to the Lamport thing is broken.

Sorry about that...

the problem is that the harsh reality is that those who claim to have and follow a spec -- in the anal bduf connotation of the term "spec" -- end up making the wrong thing or spending too much or taking too long or work-to-rule.

of course, those who go too far the other way...

:-)

Lamport contradicts himself in a significant way early on this talk. His second slides says:

When to think [...] Before writing any code.

The very next slide is titled "How to think", and promotes writing as critical to clear thinking. This is an excellent point, but writing for Lamport apparently includes writing natural language, as well as drawing blueprints and writing specifications, but it doesn't include writing code - since he repeatedly says you have to think "before writing any code".

He doesn't address or even seem to notice that he's using the word "writing" in two diametrically opposed ways - in one case, writing is a good thing that helps thinking, and in the other case, writing is something we should avoid until we've done our thinking.

This position is perhaps rooted in the context of lowish-level languages like C, which don't do much to help you think or easily express or check your thoughts. When using a low-level, machine-oriented language, it can make sense to write a specification first, without any coding involved. The programmer's job becomes that of a translator between the specification and a language that's seen as a kind of necessary evil needed to instruct the machine. And of course, most systems-level programming in the real world still works like this.

But in general, the idea that writing code must be preceded by a specification, and should not be part of the thinking process that leads to the specification, is an error which makes it difficult to use this talk as a starting point for discussion, since it's "not even wrong." It needs to be completely reframed. For example, perhaps we should be discussing the distinction between specificational code and behavioral code, and whether and how the two should be separated; and whether separate specification languages are essential for this purpose.

Writing code in a high-level language can help one think more clearly in exactly the same way that writing natural language or drawing blueprints can. Once one recognizes this, the idea that one must think and write specifications "before writing any code" is misleading at best. In some cases, developing and writing specifications can be the same thing as writing code, and this needs to be taken into account in a good discussion of the issue.

In fact, Lamport makes this case himself in talking about his TLA+ specification language. Writing TLA+ code is the good kind of writing, for Lamport, the kind that helps you think clearly. This underscores that his dichotomy between writing that helps thinking and writing that should be deferred until the thinking is done is, in fact, about the nature of the language being written. For him, it's OK to write code while specifying, if that code is sufficiently high-level, like the mathematical code of TLA+.

Well, we now have programming languages, not just specification languages, which can be very useful in prototyping high-level specifications, writing executable specifications, and even evolving those into actual programs. Unfortunately, Lamport seems unaware of this, despite having developed an essentially functional specification language of his own.

There's a slide at 39:30 of which he says "you can't write a next-state relation like this in any conventional programming language." He then shows that it can be transliterated to TLA+. But it also could quite easily be transliterated into a functional programming language.

His example of his own use of an informal specification in an actual program was disappointing. The example was a rule interpreter, in which the rule language itself was informally specified in comments. The rules were interpreted in Java, and apparently not reified at a high level in code. An implicit part of his justification of the lack of a formal spec here is that the effort needed to write such a spec in a specification language was not warranted. Here, Lamport inadvertently makes the case that having a separate formal specification language can be a disadvantage, that leads to reliance on informal specifications and low-level approaches.

In a functional language (and probably even in Java), such a program could easily have been written as a rule DSL, where an executable denotational specification for the rule language could have doubled as the actual interpreter for the language. (There's an issue here about the useful redundancy of having a specification that's separate from the program, but really we can't even get into discussing such things until we've reframed the discussion to take into account programming languages that can express specifications.)

None of the above is intended to be anti-specification - good specifications can be critical. Lamport makes some good points about the benefits of specifications. But his dichotomy between writing specifications and writing code is poorly drawn, reflecting the limitations of the tools being assumed.

In the limit, the attempt to divide the task of programming into a clear separation between writing specifications and writing code already has a notorious name: "waterfall". This model tends to fail precisely because, to paraphrase the Guindon quote on the first slide, coding is nature's way of letting you know how sloppy your thinking is. The reality of successful projects in the real world tends to be much more iterative, and that iteration involves an interleaved combination of thinking, specifying, writing code, testing, releasing, using, and repeating. Having high-level languages that can be useful early on in that process is a huge advantage, for the exact reasons that Lamport describes in the second slide.

There's also an important point here about separating specifications from programs - distinguishing between describing what a program should do and how it should do it - but again, Lamport's treatment doesn't address this point in a way that's directly relevant to higher level languages. For example, he asks "How do you connect the specs to the code?" and goes into the issue of connecting "the mathematics" of a specification to "the code", which is a dichotomy that assumes machine-oriented, un-mathematical programming languages.

Overall, the idea that writing code is a strictly post-specification activity is a dangerous radioactive monster from the 1950s which needs to have a poisoned stake driven through its heart. With all due respect to Leslie Lamport, who is a great computer scientist and programmer. But he should learn Haskell.