As CS was originally born largely from people with math backgrounds, formal proofs were all the rage for software early on. As time passed and software became more complex, that requirement effectively dropped off to some academia and defense/high-risk (aka nuclear controls) projects.

Now amazon is trying to formally verify a lot of AWS with TLA+ and other techniques. Here Mozilla is trying to verify it’s crypto.

Given the increasing rise of cyber security problems and their consequences, will formal verifications once again become more standard in software engineering? At minimum, we’ll need to see more user-friendly variants of TLA+ and other techniques for average developers to be able to use. Probably it should be taught in normal CS education. Even better would be for some kind of AI to help take existing code or specs and put it into something that can be formally proved.