The grand challenge of program verification and synthesis is to enable programmers to write programs and have assurance that the result is correct. Work since the foundation of the field has aimed to solve this challenge. Yet in practice, programmers are left to tackle critical programming problems with inadequate support from programming tools. In particular,
1. Companies continuously run wasteful sets of database queries with enormous computational costs, in part because they do not have automated methods for identifying redundant queries;
2. Parsers for practical data formats are often developed manually (and as a result, inevitably contain errors), in part because foundational approaches for synthesizing parsers cannot capture the critical features of actual formats in use;
3. Secure computations between mutually-distrusting parties can only be implemented by a small handful of cryptography experts, in part because of the mismatch between program representations directly supported by cryptographic protocols and the language constructs needed to implement practical tasks.
In this talk, I will present recent and planned work that I am performing with colleagues at Galois Inc. and an array of academic institutions that aims to address these problems. Taken broadly, our work illustrates the unique challenges that arise when making program verification work in practice.