[2026] The Way of Types: A Report on Developer Experience with Type-Driven Development

in collaboration with: Andy Zaidman Jesper Cockx

Static type systems are a well-established tool for preventing basic software errors, with more advanced ones providing strong guarantees of program correctness. Additionally, type systems encourage a “types first, implementation later” developer workflow known as “type-driven development” (TyDD). However, current widespread TyDD practices are based on simple type systems with limited expressivity, and the advanced tools being developed by researchers are not making it into mainstream programming languages. To determine how current practitioners experience the use of type-driven development and what inhibits its adoption by a wider range of developers, we conducted a survey with 130 participants from various backgrounds, asking them to describe their experience with current TyDD tools. According to them, TyDD can guide, communicate, and verify program implementation, but is currently limited by usability issues and missing features. Based on these results, we recommend that advanced TyDD tools be made available to a wider range of developers by investigating and addressing these limitations, with a focus on increasing expressivity while preserving usability.

ICPC '26

Pre-Print

[2025] Property-Based Testing Across Four Environments in Open-Source Repositories

in collaboration with: Harald Toth Antonios Barotsis Andreea Costea

Property-based testing (PBT) is a valuable technique for assessing software correctness, and its adoption differs across contexts. In this work, we examine how PBT is used in open-source repositories across three languages and four frameworks: Java with jqwik, Python with Hypothesis, and Rust with proptest and QuickCheck. Our study reveals that PBT is used to test a variety of systems and usually verifies one of the following properties: adherence to a contract, equivalence with an oracle, or expected behaviour of errors. We found that developers use a combination of customised generators and post-hoc alterations to control the property input, and they write non-trivial logic to verify the properties, often with multiple assertions along various execution paths. Though these patterns are common across the four environments, notable differences emerge from the specific tooling support of each framework and the capabilities of the underlying language. Based on these similarities and differences, our findings point to potential research directions aimed at facilitating developer adoption of PBT.

Pre-Print

[2025] Pinpointing the Learning Obstacles of an Interactive Theorem Prover

in collaboration with: Andy Zaidman Jesper Cockx

Interactive theorem provers (ITPs) are programming languages which allow users to reason about and verify their programs. Although they promise strong correctness guarantees and expressive type annotations which can act as code summaries, they tend to have a steep learning curve and poor usability. Unfortunately, there is only a vague understanding of the underlying causes for these problems within the research community. To pinpoint the exact usability bottlenecks of ITPs, we conducted an online survey among 41 computer science bachelor students, asking them to reflect on the experience of learning to use the Agda ITP and to list the obstacles they faced during the process. Qualitative analysis of the responses revealed confusion among the participants about the role of ITPs within software development processes as well as design choices and tool deficiencies which do not provide an adequate level of support to ITP users. To make ITPs more accessible to new users, we recommend that ITP designers look beyond the language itself and also consider its wider contexts of tooling, developer environments, and larger software development processes.

ICPC '25 (Distinguished Paper Award)

Pre-Print DOI

[2024] How Novices Perceive Interactive Theorem Provers (Extended Abstract)

Interactive theorem provers (ITPs) are known to have a steep learning curve and poor usability. This hinders their spread into commercial software development, wasting their potential to improve software quality. To understand what makes them inaccessible to novices, we conducted an online survey among bachelor students, asking them to list the obstacles they encountered while learning Agda. Analysis of the results revealed design choices and tool deficiencies which do not provide an adequate level of support to beginner nor advanced users. These observations point to one prominent point of improvement: providing a more accessible and sturdy infrastructure for ITP programmers.

ICFP SRC '24 (Second Place)
TyDe '24

Extended Abstract TyDe Talk Poster Slides Haskell Interlude

[2023] Bringing Formal Verification into Widespread Programming Language Ecosystems (MSc Thesis)

Formal verification is a powerful tool for ensuring program correctness but is often hard to learn to use and has not yet spread into the commercial world. This thesis focuses on finding an easy-to-use solution to make formal verification available in popular programming language ecosystems. We propose a solution where users can write code in an interactive theorem prover and then transpile it into a more popular programming language. We use Agda2HS as a case study to determine what challenges users find in using such a tool, improve selected features, and then conduct a user study to evaluate the usability. We find that detailed documentation, support for commonly-used features in the target programming language, features that facilitate verification, integration of the tool into the target ecosystem, and user studies are necessary for the accessibility of such a tool.

TU Delft

Repository