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.

Avatar photo

Posted by

is a mathematician from Manchester, UK. He worked at The University of Manchester researching finite group theory until 2012. He now works as a data analyst, is an occasional cryptic crossword setter and blogs about maths at The Aperiodical.


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

    Nicht nur der macht diesen Unterschied.
    Programme bauen Anwendungs-Situationen nach, unterstützen sie und sind sozusagen ein soziales Bild, wenn sie soziale Abläufe unterstützen. – Programme entstehen nicht aus Willkür, sondern verfolgen einen Zweck, oft, aber nicht immer, einen sozialen, manchmal im direkt Wirtschaftlichen.

    Algorithmik, kein Bär oder Mensch weiß genau, was dieser Begriff meint, er ist etymologisch sozusagen auf das Beste unscharf, meint die Mathematik, die nackte Mathematik sozusagen, ist dort auch ein Fachbereich.

    Anwendungsentwickler dürfen bis müssen diese Unterscheidung kennen.
    Schichtentrennung bleibt wichtich.

    MFG + schöne Mittwoche noch,
    Dr. Webbaer

  2. Bonuskommentar hierzu :

    “If You’re Not Writing a Program, Don’t Use a Programming Language”

    Es gibt (auch hier) eine Dreischichtigkeit der Trennung, die Anforderungslage ist (deutschsprachig) in sog. Lasten- oder Pflichtenheften zu entwickeln, der “Nachbau der Realität” in puncto IT als “Programm” und insbesondere komplexe Logik in sozusagen reiner Mathematik.

    Insofern stehen in Unternehmen der Wirtschaft auch Fachkräfte für alle drei Schichten bereit, wobei es sozusagen noch eine vierte Schicht gibt, die Anforderungen der Entscheider, oft von der Vorstandsebene, in für (noch wirtschaftsnahe) Fachkräfte verständliche o.g. Hefte zu übersetzen haben.
    Witzigerweise dürfen Dokumentationen von Software bereits entwickelt werden, von nicht direkten Fachkräften der IT, wenn die Entwicklungsarbeit noch nicht angefangen hat.

  3. Yes, Algorithms should be described as general as possible and yes, mathematically described algorithmus allow thinking, transforming and manipulating algorithms – the same is not true for code which realizes an algorithm.

    Today, in the age of artificial Intelligence, one expects that an AI-program can generate code from a mathematically described algorithm.