We live in an era of unprecedented compute availability. The advent of the cloud allows anyone to deploy critical high-performance applications that serve millions of users without owning or managing any computational resources. The goal of my research is to enable the development of such high-performance applications with robust correctness guarantees. To achieve this goal, I build practical programmable software systems that target realistic workloads in widely-used environments. My systems are rooted in solid foundations, incorporating formal specifications and techniques drawn from the programming languages, compilers, and formal methods literature.