Build systems are a fundamental part of software construction, but their correctness has received comparatively little attention, relative to more prominent parts of the toolchain. In this paper, we address the correctness of \emph{forward build systems}, which automatically determine the dependency structure of the build, rather than having it specified by the programmer.

We first define what it means for a forward build system to be correct—it must behave identically to simply executing the programmer-specified commands in order. Of course, realistic build systems employ memoization, speculation, and parallel execution, and we prove that these optimizations, as embodied in the recent forward build system \textsc{Rattle}, preserve our definition of correctness. Along the way, we show that other forward build systems, such as \textsc{Fabricate} or \textsc{Memoize}, are also correct.

We carry out all of our work in Agda, and describe in detail the assumptions underlying both \textsc{Rattle} itself and our modeling of it.