Languages, Tools, and Interfaces for Safer Code Evolution

Abstract

Evolution is the essence of software. This work argues that the burden of code evolution should be addressed at the level of languages and tools, not individual programmers. We discuss this goal through the lens of three complementary contributions. First, we present Persimmon, a functional language design with built-in extensibility features, such as extensible variant types and extensible pattern matching, powered by nested family polymorphism. Persimmon highlights how the support for code evolution, and specifically extensible programming, can be built into languages by design. Second, we focus on the generative power of large language models to assist in the verification of evolving software. We present Dafny Sketcher, a neurosymbolic framework for automated Dafny proof synthesis, and use it to show a scaffolding paradox: building on proof skeletons from reference solutions does not meaningfully improve proof generation. We explore some mitigating strategies to assess the effect of guidance when coupled with a solution sketch. Finally, we consider the human aspects of automated proof synthesis, by exploring how users interact with different tool interfaces during a proof task. Our study highlights some tradeoffs that users contend with between interface usefulness and output reliability. These results inform future designs of tool interfaces enabling co-evolution of code and proofs. Together, these contributions showcase how safer code evolution can live within our languages, tools, and interfaces.