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

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.

What would I be doing?

We have a pool of ITP programmers willing to participate in a think-aloud programming session and a consequent semi-structured interview. You would be analysing these interviews according to the techniques of the basic stage of Socio-Technical Grounded Theory (see the Further Reading below) and looking for patterns and interesting aspects of how ITP programmers write code. You can conduct the interviews yourself, together with the supervisor, or simply consult with the supervisor beforehand about the interview and let them conduct it. The result of your work would be hypotheses and emerging theories grounded in the data collected during the interviews.

Further Reading

• Related Work:
  • How Novices Perceive Interactive Theorem Provers
• 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)

Contacts for the Project

• Sára Juhošová
• Jesper Cockx