A Grounded Theory Study of "How Interactive Theorem Prover Programmers Write Code"
Master Project of Ruben Backx

Project Description

Interactive theorem provers (ITPs) such as Agda, Coq, or Lean promise formally verified software and type-driven development with interactive features. Unfortunately, they are known to be difficult to use, with a steep learning curve and an expensive development process. Additionally, ITPs have not been studied from a user perspective, meaning that we do not know where to start and what to prioritise when improving their usability.

What is the goal of this project?

The goal of this project is to examine how current ITP users actually write programs in their ITPs, which aspects they use, which aspects they like, and which aspects they would like to see improved. Since we do not know exactly what the research question is and would like to explore how ITP programmers write code, we propose a Grounded Theory study on this topic.

What is Grounded Theory?

Grounded Theory is a research methodology often used with qualitative data like interviews, intended for answering how and why questions. It involves constructing hypotheses and theories by iteratively collecting and analysing data. Instead of first constructing a hypothesis and then either supporting or falsifying it with some experiment, Grounded Theory studies use inductive reasoning to “discover” hypotheses and theories “grounded” in the data.

Further Reading

• Related Work:
  • Pinpointing the Learning Obstacles of an Interactive Theorem Prover
• On Grounded Theory:
  • Socio-Technical Grounded Theory for Software Engineering by Rashina Hoda (2022)
  • Grounded theory in software engineering research: a critical review and guidelines by Stol et al. (2016)
• Similar Work:
  • How statically-typed functional programmers write code by Lubin and Chasins (2021)
  • Real World Scrum: A Grounded Theory of Variations in Practice by Masood et al. (2022)