The dream of building provably correct software seems to be coming closer to reality. It is very cool to see all the recent work on the systems community on building provably correct systems components.
At the same time, I’m worried that the training of software developers actually involves less formal logic compared to a generation ago. There is so much more computer science to teach in college, and formal logic has been squeezed into a smaller fraction of the curriculum. That fact doesn’t bode well for future adoption of formal methods to build more reliable, secure software. Maybe there will be enough highly trained developers to build core systems components (e.g., hypervisors) to a high standard, but many security vulnerabilities are at the application level.