• Curry On Talk: The Practice and Theory of TLA+

    My Curry On talk about TLA+

  • TLA+ in Practice and Theory
    Part 4: Order in TLA+

    We learn how to encapsulate and compose TLA+ specifications, of the precise mathematical definition of abstraction, and compare TLA+'s notion of abstraction with those of other formalisms. Plus some various cool stuff.

  • TLA+ in Practice and Theory
    Part 3: The (Temporal) Logic of Actions

    TLA, the Temporal Logic of Actions is the core of TLA+. It is a temporal logic that minimizes the use of temporal reasoning in favor of more ordinary mathematics. It is a general mathematical framework for describing and reasoning about algorithms and systems.

  • TLA+ in Practice and Theory
    Part 2: The + in TLA+

    We explore the "data logic" of TLA+, the means by which TLA+ specifications describe a state of computation: its data structures. To do that, we first cover the basics of mathematical logic.

  • TLA+ in Practice and Theory
    Part 1: The Principles of TLA+

    TLA+ is a formal specification and verification language intended to help engineers specify, design and reason about complex, real-life algorithms and software or hardware systems. We explore its motivation, application and principles of design.

  • The Best Programming Language

    Programming languages cannot be judged on intrinsic qualities alone.

  • What We Talk About When We Talk About Computation

    Machine and language models of computation differ so greatly in the computational complexity properties of their representation that they form two distinct classes that cannot be directly compared in a meaningful way. While machine models are self-contained, the properties of the language models indicate that they require a computationally powerful collaborator, and are better called models of programming.

  • Why Writing Correct Software Is Hard

    We try to understand the relationship between programs and correctness, and in particular, why writing correct programs must be hard. We will review results from computability theory and complexity theory, and see that programs and complete understanding – which is required for correctness – are fundamentally at odds.