MIT 6.512, Fall 2025
* Our department at MIT is in the midst of a global subject renumbering, so the official number is 6.5120, ending in a zero that will be removed in a few years. Briefly, this course is about an approach to bringing software engineering up-to-speed with more traditional engineering disciplines, providing a mathematical foundation for rigorous analysis of realistic computer systems. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave properly. As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments. We will learn how to apply these tools to certify that programs behave as expected. More specifically: Introductions to two intertangled subjects: the Rocq proof assistant, a tool for machine-checked mathematical theorem proving; and formal logical reasoning about the correct
Explore this link on the map →