Gradual Enforcement of Program Invariants

摘要

Static and dynamic techniques have long been used to check and enforce properties of program executions. They are often seen as diametrically opposed, as exemplified by the long-running kerfuffle over the merits and deficits of static versus dynamic type checking. Recently, PL researchers and designers have sought to bridge the divide between these approaches to program checking and analysis. In particular, gradual typing sets out to seamlessly combine static and dynamic checking of how closely programs adhere to standard typing disciplines from the literature. In this context, static and dynamic checking and enforcement are treated as complementary rather than conflicting. In this talk 1 will discuss the theory and practice of gradual typing. Both have undergone significant development in the last few years. These advances in language design change not only how dynamic and static checking can work together, but also change how we think about each individually.