Build System Correctness
Intuitively: when a build system updates all the correct dependencies and target.
Formally: Given a build system, its tasks, a target key, an initial store, and a result store. The build system is correct if:
- No inputs were corrupted during the build.
forall input keys: getValue k result_store == getValue k initial_store
- The result is consistent with the tasks. Recomputing tasks doesn’t change anything.
forall output keys: getValue k result_store == compute task result_store
A build system is correct if it produces a correct result store for any tasks, target key, and initial store. This correctness property is very difficult when cyclic tasks are given.
Important: The formal definition does not hold for non-deterministic tasks and shallow cloud builds. However, the general principle still applies.