Leslie Lamport Thinks Your Code Is Bad

At last year’s HLF, Turing Award Leslie Lamport gave us his (not wholly complimentary) thoughts on the state of proof-writing in mathematics. Since he has worked in both maths and computer science, members of the latter discipline may have felt they got off quite lightly. Perhaps to redress the balance, this year we found out what he thinks is wrong with most people’s code and algorithms, in a talk titled If You’re Not Writing a Program, Don’t Use a Programming Language.

Lamport made a distinction between programs and algorithms: programs are the real-world code written in programming languages, while an algorithm is the underlying abstract concept. He paraphrases fellow Turing laureate Tony Hoare to summarise the situation: “inside every large program is an algorithm trying to get out”. The problem as Lamport sees it is that too often, people try to verify their algorithms at the level of the program, where the algorithm is obscured by the messy details of the code: the variable types, the attention to edge cases and so on.

In an article for Wired, he analogises the situation to another field: “Architects don’t make their blueprints out of bricks.” – and they certainly don’t press on without making a blueprint at all.

In my days as a PhD student working on problems related to computational group theory, I grappled with the problem of demonstrating the correctness of an algorithm, while at the same time giving a comprehensible overview of how it works in the event that anyone might one day want to actually implement it. So, while by no stretch of the imagination being a computer scientist or even a serious coder, I can appreciate that this problem is real and non-trivial to solve.

So what is the solution? Lamport says we should describe our algorithms not with code – real or pseudo – but with mathematics. Lamport shows us how to encode an algorithm in a set of predicates: logical statements describing the initial state of the algorithm, the transitions between subsequent states, and the required outputs and conditions for the algorithm to terminate. Treating algorithms as mathematics allows us to more easily appreciate their overall structure, and to successfully ‘debug’ them. He’s involved with a system called TLA which implements this idea.

Via a brief detour into topology, Lamport backs up the credentials for his system with quotes from some of the big guns – Microsoft and Amazon Web Services. While I suspect that his desired revolution in mathematical proof may be a long time coming, it seems like his ideas on improving algorithms have some friends in high places.

You can watch the talk on the HLF website.