Programs and Proofs in Practice: A Grounded Theory on How People Program with Dependent Types

Abstract

Dependently typed programming languages (DTPLs) are powerful tools that help improve software correctness. However, they currently serve niche communities, and have not yet been adopted in mainstream software development processes. Through this work, we aim to understand how people program in dependently typed languages to provide a solid, layered understanding of the starting point for any future advancements in DTPL design. We apply the small-scale, emergent-mode Socio-Technical Grounded Theory methodology to develop a theory grounded in data from interviews conducted with DTPL users with varying levels of experience, using Agda, Rocq, and Lean. Our results show how DTPL programmers use types to plan and constrain their programs; make trade-offs in how they represent data; and continuously interact with the compiler to construct a program iteratively. Based on our findings, we have formulated five recommendations for the developers and maintainers of DTPLs who wish to make their work more accessible to a broader audience of software developers.