Improving the usability and accessibility of dependently typed programming languages
Master Project

Thesis

https://resolver.tudelft.nl/uuid:0a13ca4a-9d3c-416e-bb88-affc3f14ee52

Problem statement

Dependently typed programming languages such as Agda offer the programmer the ability to express precise invariants at the type level, and even to write full formal proofs of their program’s correctness. However, they are also often considered to be hard to learn and use. As a result, their usage in practical software development remains very limited.

Project description

The goal of this project is to investigate one or more aspects of the implementation of Agda that have a large impact on its usability and accessibility, such as the design of its syntax, error messages, and editor integration. One particular point of attention is how unsolved metavariables are reported back to the user in case they could not be solved by Agda.

After investigating potential issues with usability, you will implement an improvement to one or more of these issues, and ideally evaluate the impact of this improvement through a small user study.

Further reading

• Sára Juhošová, Andy Zaidman, and Jesper Cockx: Pinpointing the Learning Obstacles of an Interactive Theorem Prover (2025)
• Sára Juhošová, Andy Zaidman, and Jesper Cockx: The Way of Types: A Report on Developer Experience with Type-Driven Development (2026)

Contacts for the project

• Jesper Cockx (TU Delft)