Curry On
Barcelona!
June 19-20th, 2017


The Practice and Theory of TLA+
Ron Pressler
Oracle + Parallel Universe

@pressron


Abstract

“Thinking is not the ability to manipulate language; it’s the ability to manipulate concepts. Computer science should be about concepts, not languages. But how does one teach concepts without getting distracted by the language in which those concepts are expressed? My answer is to use the same language as every other branch of science and engineering — namely, mathematics.” — Leslie Lamport. Leslie Lamport’s TLA+ is a mathematical formalism designed as a specification and verification language for software and hardware systems. Its simplicity and power allow it to be used to reason about many different kinds of algorithms — sequential, concurrent, parallel or distributed — within a single conceptual framework, to scale to large, complex, real-world systems, and to be used by “ordinary” engineers. As a result, it has been successfully applied at Amazon, Microsoft, Intel, Oracle and other companies as a formal method for the verification of complex real-world hardware and software designs of commercial products, without requiring close assistance from academic experts. TLA+ achieves this rare combination of power and simplicity by describing algorithms, systems and their properties not in a programming language, but with ordinary mathematics (as much as possible). Just as ordinary differential equations are a universal tool for reasoning about continuous dynamical systems, TLA+ is a universal tool for reasoning about discrete dynamical processes, of which software and hardware are just two examples. In this talk I will try to show how pragmatism shaped TLA+’s theory and design, explore how it gives precise meaning to concepts like abstraction and implementation (refinement), and compare it with approaches to formal specification based on programming language theory (like dependent types) for which TLA+ offers a radically different, refreshing alternative.

Bio

Ron Pressler is a veteran software developer. He is the founder of Parallel Universe, which makes open source infrastructure software, and works at Oracle on the Java platform.