Excellent course, the future of solid software looks bright.
https://frap.csail.mit.edu/main
"What's it all about?
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."
Optimistic rant
@zpartacoos It is a new decade. There have been some serious breakthroughs.
The common programmer might have a tough time competing with data assisted program synthesis, and programmers that can wield the dependent types to control that synthesis.
Optimistic rant
@jmw150 hm when you say data assisted program synthesis is that it's own field separate from FM or is that a fancy way of saying "Machine Learning"? Please clarify.
Also, would you say that course is a good place to brush up on modern FM? Are you aware of other resources on the latest stuff?
Optimistic rant
@zpartacoos Machine learning and program synthesis are related fields, but not completely the same. Program synthesis is also not completely separate from FM either.
It is an intro graduate course, so it is a good place to start from scratch. But to brush up, some survey research papers would be better.
Program synthesis (as of 2017)
https://www.microsoft.com/en-us/research/wp-content/uploads/2017/10/program_synthesis_now.pdf
Also FM and ML being used together (this April)
https://arxiv.org/pdf/2104.02466.pdf
Deranged rant
@jmw150 why do formal methods professors keep over hyping their courses?
We've had automated proof assistants as well as a lot of the mathematical paradigms mentioned in the course (Pi-calculus and its many variants, lambda calculus, Coq, etc.) For many many years...yet software is still brittle and few people use these tools/mathematical frameworks. Typically, you only see them in defense companies or banks. So, why lie to the students telling them they can guarantee "safe" code when in reality very few students will actually use these methods in practice? The fast pace of software companies rarely allows for deep analysis of a program. When you're in the 100,000+ code lines then none of this stuff is particularly useful.
On the bright side, I'm glad we have the formal methods folks as without them we wouldn't have safe airplanes, medical devices , etc...