Guaranteed Optimization is a new technique for building compilers that have proven guarantees of what optimizations they perform. Such compilers produce programs that are optimal with respect to certain criteria, such as program size or static operation counts. This optimality result is relative to an approximate program quivalence, exact program equivalence being, of course, undecidable. Guaranteed optimization compilers have a well-defined `kernel', which may roughly be thought of as defining what code is evaluated and erased at compile-time (similar to a binding time specification). The kernel is proven to encompass certain `de-optimizing rewrites' that make programs worse. These rewrites define a closure property of the kernel: any amount of de-optimization can be applied to a source program, and the compiler is guaranteed to undo it all in a single pass. By choosing rewrites that capture common patterns of software engineering abstraction, one can construct compilers that reliably reduce the `abstraction penalty' associated with high-level languages. The de-optimizing rewrites give programmers and language designers an intuitive guarantee of what transformations the compiler has been verified to undo.