Abstract
Physical theories as usually formulated consist of a mathematical description and a set of (often implicit) guidelines/‘rules of thumb’ for their application. In the case of the thermodynamics of a single particle in a box, the simple equations for behaviour are generally accepted, but differences in their application lead to extreme disagreements; most notably, whether the Second Law can be violated. We introduce a programming language to describe these simple thermodynamic processes, and give an operational semantics and program logic as a basis for formal reasoning about such simple thermodynamic systems. By finding a computational invarient of the system, we prove that all possible combinations of basic operations must preserve the Second Law. Moreover, the same invariant determines a cost to information erasure: Landauer Erasure becomes a theorem of the formal system. This method of formalising both the mathematical and logical structures of physical processes will have applications to many different areas of physics.