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