QED in Context: An Observation Study of Proof Assistant Users

How they used Delve

HCI and programming-languages researchers at the University of Pennsylvania used Delve for the open coding pass of a thematic analysis of roughly 43 hours of observation transcripts from 30 Rocq and Lean users, producing the codebook behind a POPL paper on what proof assistant use really looks like.

“The first author then conducted a thematic analysis [10] of the transcripts. This analysis involved an initial open coding pass using the Delve qualitative coding tool [23]. In this pass, the author reviewed transcripts for interesting patterns of usage and tagged them with codes. These codes were updated throughout analysis for consistency and completeness.”

Field

Human-computer interaction and programming languages; how experts actually work with interactive theorem provers (Rocq and Lean) in their everyday practice

Data

About 43 hours of screen-and-audio session recordings from 30 proof assistant users working in Rocq and Lean on their own everyday tasks, auto-transcribed by Zoom and then heavily revised by two authors to fix transcription errors and embed notes on participants' actions and the code they were working with

Approach

Contextual inquiry: participants were observed doing their own everyday proof work. Analysis was a thematic analysis run in two passes - an initial open coding pass in Delve tagging patterns of usage, with codes revised throughout for consistency and completeness, then a second axial pass applying the revised codebook. The whole authoring team reviewed examples and the codebook in meetings and asynchronous review; once about 75% of transcripts were coded, another author audited the analysis by spot-checking excerpts for every code, and all examples were checked back against the video recordings.

Data types

Observation