  In Racket, the LLVM IR, Rust, and other modern languages, programmers and
static analyses can hint, with special annotations, that certain parts of a
program are unreachable. Same as other assumptions about undefined behavior;
the compiler assumes these hints are correct and transforms the program
aggressively.
  While compile-time transformations due to undefined behavior often perplex
compiler writers and developers, we show that the essence of transformations
due to unreachable code can be distilled in a surprisingly small set of simple
formal rules. Specifically, following the well-established tradition of
understanding linguistic phenomena through calculi, we introduce the first
calculus for unreachable. Its term-rewriting rules that take advantage of
unreachable fall into two groups. The first group allows the compiler to delete
any code downstream of unreachable, and any effect-free code upstream of
unreachable. The second group consists of rules that eliminate conditional
expressions when one of their branches is unreachable. We show the correctness
of the rules with a novel logical relation, and we examine how they correspond
to transformations due to unreachable in Racket and LLVM.
