From Scripting to Proving: Gradual Verification for Expressive Programming Languages

Programmers are rapidly adopting expressive, dynamically typed,higher-order functional programming languages for their everydaydevelopment tasks. Over time, these programs are often fortified withstatic type checking by migrating programs using gradual types, atechnique now widely used by the largest industrial softwaredevelopment companies. Unfortunately, there are limits both to whatproperties gradual types can validate and the help they can provideprograms as they engage in the migration process. In parallel,researchers have developed sophisticated next generation programminglanguages with integrated verification features. These languages areable to validate much stronger claims about the correctness ofsoftware, but their industrial adoption has lagged far behind gradualtyping. Consequently, verification is not being integrated in theeveryday lives of programmers and the quality and reliability ofsoftware suffers because of it. This represents a tremendous missedopportunity considering the rapid advancement of automatedverification techniques.In this talk, I will give an overview of my group's recent efforts toclose the expressivity gap between commonplace scripting languages andrarefied verification-integrated languages, enabling pathways toverified programming at every point along the spectrum from scriptinglanguages to theorem proving languages.At the core of the technical approach is an embrace of what we dubgradual verification, a technique which leverages run-time enforcementmechanisms, for example run-time type checking or array boundschecking, and---using methods from the theory of abstractinterpretation---systematically turning these run-time methods in tostatic verification methods. Moreover, thanks to the run-time basis,verification becomes a spectrum rather than a binary, since anyproperty that fails to statically verify can be enforced by theunderlying run-time mechanism. This approach enables programs toevolve over time from less- to more-verified gradient and opens up thepossibility for a number of useful programming tools.