Correctness of Compilers: Part 1

This lecture explores the correctness of compilers, focusing on defining correctness, compiler projects, expression language correctness, and proving correctness using the Stainless verifier for Scala. It discusses examples of verified compilers like CompCert, CakeML, and Bedrock2, as well as the concepts of certified compilers versus compilers proven correct. The lecture also delves into formal verification, program enumeration for rigorous compiler testing, and the importance of ensuring compilers generate correct programs. It covers the process of compiling to a stack machine, interpreting expressions, and running compiled programs. The instructor emphasizes the significance of formal verification in establishing program correctness and the challenges associated with certifying compilers.