Programmers are rapidly adopting expressive, dynamically typed,
higher-order functional programming languages for their everyday
development tasks. Over time, these programs are often fortified with
static type checking by migrating programs using gradual types, a
technique now widely used by the largest industrial software
development companies. Unfortunately, there are limits both to what
properties gradual types can validate and the help they can provide
programs as they engage in the migration process. In parallel,
researchers have developed sophisticated next generation programming
languages with integrated verification features. These languages are
able to validate much stronger claims about the correctness of
software, but their industrial adoption has lagged far behind gradual
typing. Consequently, verification is not being integrated in the
everyday lives of programmers and the quality and reliability of
software suffers because of it. This represents a tremendous missed
opportunity considering the rapid advancement of automated
verification techniques.
In this talk, I will give an overview of my group's recent efforts to
close the expressivity gap between commonplace scripting languages and
rarefied verification-integrated languages, enabling pathways to
verified programming at every point along the spectrum from scripting
languages to theorem proving languages.
At the core of the technical approach is an embrace of what we dub
gradual verification, a technique which leverages run-time enforcement
mechanisms, for example run-time type checking or array bounds
checking, and---using methods from the theory of abstract
interpretation---
static verification methods. Moreover, thanks to the run-time basis,
verification becomes a spectrum rather than a binary, since any
property that fails to statically verify can be enforced by the
underlying run-time mechanism. This approach enables programs to
evolve over time from less- to more-verified gradient and opens up the
possibility for a number of useful programming tools.
I work toward making the construction of reusable, trusted software
components possible and effective. My research has spanned program
analysis; semantics; verification and model-checking; security; logic;
complexity; and algorithms.
With Jeff Foster and Mike Hicks, I direct the laboratory for
Programming Languagesat the University of Maryland (PLUM).
Previously, I’ve worked with the Programming Research Laboratory (PRL)
at Northeastern University.
I co-authored the book Realm of Racket with Matthias Felleisen
and undergraduates from Northeastern University, which introduces
programming interactive video games.