How Tests and Proofs Impede One Another: The Need for Always-On Static and Dynamic Feedback

Abstract

Dynamic and static feedback provide complementary benefits, and neither one dominates the other. Sometimes, sound global static checking is most useful. At other times, running tests is most useful. Unfortunately, current languages impose too rigid a model of the development process: they favor either static or dynamic tools, which prevents the programmer from freely using the other variety. I propose a new approach, in which the developer always has access to immediate execution feedback, and always has access to sound static feedback. The aim is to permit developers to work the way they find most natural and effective, which will improve reliability and reduce cost. Developers will create software that is more reliable than that created in an environment that favors dynamic analysis. Developers will work faster than they can in an environment that favors static analysis.