Senior Submission
There are two compiler universes. In universe Σ\SigmaΣ, they statically analyze code. Its optimizers are theorem provers, that apply equivalence preserving transformations to speed up computation. Many small hints about the structure of data and computation are provided by the programmer to that end. On the other hand, in universe Ω\OmegaΩ programs are hard to analyze statically. Here, optimizers are anthropologists; they observe the program behavior and optimize for its predicted future. One universe bases its optimizations on facts, the other one on predictions, or even fictions. What, if they are not that different after all? Non-refutable facts are hard to come by, even in universe Σ\SigmaΣ. And from Ω\OmegaΩ we learn, that it can be very efficient to rely on fictions – as long as they are not refuted.

We propose to search for ways of integrating those two worlds. We argue that, with the proper accounting, predictions and assumptions can be used for optimizations; just like facts. Such a compiler uses optimizations which are correct ``up to some context of assumptions''. By controlling the scope of assumptions, and tracking their dependencies, target code comes with a description of a particular execution context, under which it is correct.