Most programmers associate formal verification and mechanical theorem proving with formalizing mathematics, high assurance software (such as aerospace control systems), and hardware checking, but not their own work. Yet, recently these approaches have found success in more commonplace applications such as C compilers and relational databases. We attribute this expansion to a greater appreciation of reliable software and a decrease in the cost of verification. In this talk, I will describe my own forays into this area with an emphasis on how formal verification creates practical benefits that would not have been available if not for the reliability of the theorems. I have selected a diverse set of applications for this presentation:
- how traditional network services, like load-balancers, must adapt to handle the unique constraints of cryptographic protocols;
- how simple probabilistic relationships need a foundation in complex measure theory to understand and automate;
- how modern APIs assume users obey temporal orderings in their uses which need a new kind of monitoring system to enforce at runtime.
Finally, I will close with a sketch of further ways that this application of programming language and verification research can improve software quality and programmer quality of life.