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 LanguageGiven 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.
How to Write a 21st Century ProofGiven 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.
The PlusCal Algorithm LanguageGiven 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.
A Mathematical View of Computer SystemsGiven 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 2015Given 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.
Programming Should be More than CodingGiven at Stanford University on 8 April 2015.
Abstract
Writing a program involves three tasks:
Thinking for ProgrammersGiven 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.
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.
Thinking Above the CodeGiven 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.
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.
My Papers About TLA and TLA+ [show]
A page listing approximately all the papers I've written
about TLA and TLA+.
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 CannibalsA 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 problemThis example generalizes the eight queens puzzle from 8 to N and specifies an algorithm to solve it. The fileQueens.tla contains a TLA+ spec and
QueensPluscal.tla contains a PlusCal spec.
The Prisoners ProblemA cute problem and its solution, described in the filePrisoners.tla .
Termination detection in a ringThis 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 fileEWD840.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+.
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.
Unclassifiable [show]Why Don't Computer Scientists Learn Math?Click here for an anecdote demonstrating the sad state of computer science education. |
||