Software development is an inherently incremental process. To this end, most programming languages provide basic mechanisms for programmers to indicate that a given functionality is not yet implemented, for instance through dedicated exceptions. Unfortunately, apart from incremental typecheckers, most of the tools used to reason about program correctness—like testing, analysis, and verification frameworks—fail to account for these incompleteness idioms. As a result, programmers are faced with either spurious failure reports or the burden of altering their specifications, which sacrifices the direct causal connection between the code and the reasoning tools. In this talk, I will illustrate this issue in the context of testing, considering both unit testing and property-based testing, as well as certified programming in proof assistants. Examining the problem in such disparate settings allows us to isolate the core concepts required to build truly incremental reasoning tools.
Bio:
Éric Tanter is a Full Professor in the Computer Science Department of the University of Chile. He received his PhD from both the University of Nantes and the University of Chile in 2004. His research interests cover programming languages and software engineering, ranging from the theoretical underpinnings of programming languages to the empirical study of the practice of programming. Recently, he has been deeply involved in the foundations and practice of gradual typing and verification. He holds an Inria International Chair for the period 2025-2029.