  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 avoid repeated work, stop early
when possible, and run commands in parallel, 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} and \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.
