I like the intersection of language research and implementation. I can greatly enjoy pointer arithmetic as well as working towards avoiding it.
We formalized speculative optimizations in a model IR called sourir. Speculation needs deoptimization, aka on-stack-replacement (OSR): optimizations are undone at runtime, functions replaced while being executed. We show how to construct and maintain correct deoptimization points and prove correctness of standard optimizations.