The web has become a pervasive part of our lives, giving us previously unfathomable access to information and computation. The dynamic, interactive experience of the modern web is made possible only by the substantial engineering efforts put into making web browsers run correctly and with high efficiency. Towards this aim, software engineers have crafted complex, highly specialized algorithms and tuned their performance largely through informal and experimental techniques. Web browser layout engines are a case in point; Google has 10 full-time staff members specifically dedicated to this component of Google Chrome. In our research, we set out to develop a system to transform a high-level description of such computations on a restricted domain of tree-shaped data structures into an algorithm to perform the computations on any input from this domain with both efficiency and correctness. More generally, this kind of transformation, involving the automated construction of a program from a high-level, constrained description, is known as program synthesis, or optimal program synthesis when optimization is incorporated into the process. In our case, we optimize with respect to the time necessary to compute or update a prior result based on a change in input by exploiting parallel and incremental computation. Existing, domain-specific implementations already incorporate both concepts but often suboptimally and sometimes even incorrectly, as they are notoriously difficult to get right. In our approach, we employ an automated theorem prover to perform multiple compositional searches over the space of candidate algorithms and select the optimal candidate according to our efficiency approximation methods. In the process of accomplishing this, we have created a novel approach to decomposing complex, almost intractable problems in program synthesis. Currently, we are applying this work to synthesize a highly performant web layout engine with guaranteed layout correctness.