• People Don't Write Programs

  28 Apr 2018

  When thinking about software verification, we tell ourselves a story about how people write programs. This story isn't true.

• Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra, Part III

  19 Jan 2018

  The history of computation, logic and algebra, told by primary sources. Part 3 covers the logicistic/mathematical/computational period of logic in the twentieth century.

• Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra, Part II

  12 Jan 2018

  The history of computation, logic and algebra, told by primary sources. Part 2 covers the algebraic period of logic in the nineteenth century.

• Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra, Part I

  05 Jan 2018

  The history of computation, logic and algebra, told by primary sources. Part 1 covers the classical and embryonic periods of logic, from Aristotle in the fourth century, BCE, to Euler in the eighteenth century.

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

  20 Jun 2017

  My Curry On talk about TLA⁺

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

  15 Jun 2017

  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

  08 Jun 2017

  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⁺

  01 Jun 2017

  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.