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.