Date Added: Apr 2011
Complex distributed algorithms become running systems through an integration with optimizations that target the system's deployment environment. Although expedient, this approach has disadvantages. First, this often makes implementing the algorithm difficult, since its logic must be composed with the optimizations. Second, proving the guarantees of the implementation is tedious, because the proofs must be derived for the composed algorithm, which may not be directly mappable to the original, un-optimized algorithm. Finally, retargeting the implementation to a different deployment - requiring a different set of optimizations - can be wasteful, since a new composed algorithm must be derived to include this different set of optimizations, including their correctness proofs.