flâneur

MIT 6.512, Fall 2025

frap.csail.mit.edu · 1,428 words · saved by 1 readers

* 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

Go to student portal Formal Reasoning About Programs A graduate course at MIT in Fall 2025 Subject number: 6.512* Instructor: Adam Chlipala Teaching assistant: Paul Mure Class meets: MW 2:30-4:00, 36-156 * 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. Key links: book and related source code; GitHub repo with problem sets What's it all about? Briefly, this course is about an approach to bringing software engineering up-to-speed with more traditional engineering…

saved by

related reading