More Stuff

Leslie Lamport

Last modified on 16 March 2021

You'll miss a lot on this web site unless you enable Javascript in your browser.

Videos of My Talks about Specification       [show]

If You're Not Writing a Program, Don't Use a Programming Language

Given in Heidelberg on 24 September 2018 at the 2018 Heidelberg Laureate Forum. 
Abstract  Algorithms are not programs. They can and should be written with math rather than programming languages or pseudo-languages. This applies to many more algorithms than the ones taught in algorithm courses.

[video]

How to Write a 21st Century Proof

Given in Heidelberg on 26 September 2017 at the 2017 Heidelberg Laureate Forum.
Abstract  Mathematicians have made a lot of progress in the last 350 years, but not in writing proofs. The proofs they write today are just like the ones written by Newton. This makes it all too easy to prove things that aren’t true. I’ll describe a better way that I’ve been using for more than 25 years.

[video]

The PlusCal Algorithm Language

Given in Heidelberg on 22 September 2016 at the 2016 Heidelberg Laureate Forum.
Abstract  An algorithm is not a program, so why describe it with a programming language? PlusCal is a tiny toy-like language that is infinitely more expressive than any programming language because an expression can be any mathematical formula.

[video]

A Mathematical View of Computer Systems

Given in Heidelberg on 24 August 2015 at the 2015 Heidelberg Laureate Forum and in Beijing on 28 October 2015 at the Computing in the 21st Century Conference.
Abstract  Mathematics provides what I believe to be the simplest and most powerful way to describe computer systems.

[Heidelberg video]     [Beijing video]

The Bakery Algorithm in 2015

Given in Rennes, France on 5 May 2017 at the International Workshop on Distributed Computing in the honor of Michel Raynal. 
Abstract  An algorithm is not a program, so why describe it with a programming language? PlusCal is a tiny toy-like language that is infinitely more expressive than any programming language because an expression can be any mathematical formula.

[video]     [slides]

Programming Should be More than Coding

Given at Stanford University on 8 April 2015. 
Abstract  Writing a program involves three tasks:
  1. Deciding what the program should do.
  2. Deciding how the program should do it.
  3. Coding: Implementing these decisions in code.
Too often, all three are combined into the process of coding. This talk explains why they should be separated, and discusses how to perform the first two.

[video]

Thinking for Programmers

Given in San Francisco on 3 April 2014 at the Build conference. 
Abstract  [I]ntroduces techniques and tools that help programmers think above the code level to determine what applications and services should do and ensure that they do it. Depending on the task, the appropriate tools can range from simple prose to formal, tool-checked models written in TLA+ or PlusCal.

[video]

Who Builds a Skyscraper without Drawing Blueprints?

Given in San Francisco on 19 Novembr 2014 at the React conference. 
Abstract  Architects draw detailed plans before construction begins. Software engineers don't. Can this be why buildings seldom collapse and programs often crash? A blueprint for software is called a specification. TLA+ specifications have been described as exhaustively testable pseudo-code. High-level TLA+ specifications can catch design errors that are now found only by examining the rubble after a system has collapsed.

[video]     [slides to appear]

Thinking Above the Code

Given in Redmond, Washington on 14 July 2014 at the Microsoft Faculty Summit.
Abstract  Architects draw detailed blueprints before a brick is laid or a nail is hammered. Programmers and software engineers seldom do. A blueprint for software is called a specification. The need for extremely rigorous specifications before coding complex or critical systems should be obvious--especially for concurrent and distributed systems. This talk explains why some sort of specification should be written for any software.

[video]

What is Computation?

Given in Haifa, Israel on 2 June 2011 at the Technion — Israel Institute of Technology.
A simple introduction to thinking of computations as sequences of states and thinking of computing devices as state machines that can be described with elementary math.

[video]

My Papers About TLA and TLA+       [show]

A page listing approximately all the papers I've written about TLA and TLA+.

[click here]

Examples       [show]

The TLA+ GitHub repository contains a few dozen examples of TLA+ specifications here.  They have not been edited and are of varying quality and degree of complexity.  Here are a few simple ones suitable for newcomers to TLA+.

Missionaries and Cannibals

A well-known problem is specified in TLA+ and solved with the TLC model checker.  The spec assumes knowledge of TLA+; everything you need to know is explained in comments.

The  N  queens problem

This example generalizes the eight queens puzzle from 8 to  N  and specifies an algorithm to solve it.  The file Queens.tla contains a TLA+ spec and QueensPluscal.tla contains a PlusCal spec.

The Prisoners Problem

A cute problem and its solution, described in the file Prisoners.tla.

Termination detection in a ring

This is a TLA+ specification of an algorithm of Dijkstra, Fiejen, and van Gasteren.  There is a link to Dijkstra's tech report EWD840.  Read the first page of that report to understand the problem solved by the algorithm, which is described by the spec in the file EWD840.tla.  Most people will not want to read the rest of the tech report, which provides an informal explanation of the algorithm and why it is correct, or the file EWD840_proof.tla that contains a machine-checked TLA+ correctness proof.

Videos of Paxos Lectures       [show]

Videos of two lectures describing the Paxos consensus algorithm with TLA+.  In addition to explaining the algorithm, they provide a crash course on TLA+.

[click here]

Other Relevant Links       [show]

Links to pages related to TLA+ outside the TLA+ and TLAPS web sites.  If you'd like links to your work added to this page, contact me.
Weeks of debugging can save you hours of TLA+
This is a 39-minute video by Markus Kuppe showing how writing and checking a TLA+ specification can be a much more efficient way of finding the source of a concurrency bug in a program than trying to debug the code.  It assumes no knowledge of TLA+.  Dated December 23, 2020.

Large Scale Model Checking 101
This is a video by Markus Kuppe giving practical advice on using the TLC model checker for checking large models.  Dated April 11, 2018.

TLA+ Workshops:    2020    2018    2014    2012   
These are four workshops on TLA+ held on the indicated years. Their pages list the talks that were presented, which were on all aspects of TLA+ including applications and tools.  Also included is accompanying material containing most of the slides and some accompanying papers.  The page for the 2020 workshop, which was held on-line, contains videos of most of the talks.

The Community Repository
This is an open GitHub repository dedicated to contributions from the TLA+ community.  It contains modules with definitions that you may find useful in your own TLA+ specifications.  Some have Java overrides to permit more efficient execution by the TLC model checker.  You can also submit modules containing material that you want to share with the rest of the TLA+ community.
Stephan Merz
A page containing a link to Stephan Merz's publication list, which includes several papers on TLA. 

Work With and On Lamport's TLA .
Publications by the Networks and Distributed Systems group at the University of Bielefeld, headed by Peter Ladkin.  They are all dated 1996 and 1997, but at least some of them are still worth reading.

Unclassifiable       [show]

Why Don't Computer Scientists Learn Math?

Click here for an anecdote demonstrating the sad state of computer science education.