{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T03:22:35Z","timestamp":1785381755563,"version":"3.55.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-24-C-B044"],"award-info":[{"award-number":["FA8750-24-C-B044"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Interactive theorem provers, or proof assistants, are important tools across many areas of computer science and mathematics, but even experts find them challenging to use effectively. To improve their design, we need a deeper, user-centric understanding of proof assistant usage.\n \n \n \nWe present the results of an observation study of proof assistant users. We use contextual inquiry methodology, observing 30 participants doing their everyday work in Rocq and Lean. We qualitatively analyze their experiences to surface four observations: that proof writers iterate on their proofs by reacting to and incorporating feedback from the proof assistant; that proof progress often involves challenging conversations with the proof assistant; that proofs are constructed in consultation with a wide array of external resources; and that proof writers are guided by design considerations that go beyond \"getting to QED.\" Our documentation of these themes clarifies what proof assistant usage looks like currently and identifies potential opportunities that researchers should consider when working to improve the usability of proof assistants.<\/jats:p>","DOI":"10.1145\/3720426","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"337-363","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["QED in Context: An Observation Study of Proof Assistant Users"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1507-1122","authenticated-orcid":false,"given":"Jessica","family":"Shi","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6717-9586","authenticated-orcid":false,"given":"Cassia","family":"Torczon","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9631-1169","authenticated-orcid":false,"given":"Harrison","family":"Goldstein","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, USA"},{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7839-1636","authenticated-orcid":false,"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1523-3347","authenticated-orcid":false,"given":"Andrew","family":"Head","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion58688.2023.00018"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"J. Stuart Aitken Phil Gray Tom Melham and Muffy Thomas. 1998. Interactive Theorem Proving: An Empirical Study of User Activity. In Journal of Symbolic Computation. https:\/\/doi.org\/10.1006\/jsco.1997.0175 10.1006\/jsco.1997.0175","DOI":"10.1006\/jsco.1997.0175"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Stuart Aitken and T Melham. 2000. An Analysis of Errors in Interactive Proof Attempts. In Interacting with Computers. https:\/\/doi.org\/10.1016\/S0953-5438(99)00023-5 10.1016\/S0953-5438(99)00023-5","DOI":"10.1016\/S0953-5438(99)00023-5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227120"},{"key":"e_1_2_1_6_1","unstructured":"Jeremy Avigad and Patrick Massot. 2020. Mathematics in Lean. Electronic Textbook. https:\/\/leanprover-community.github.io\/mathematics_in_lean"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586030"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Bernhard Beckert Sarah Grebing and Florian B\u00f6hl. 2015. A Usability Evaluation of Interactive Theorem Provers Using Focus Groups. In Software Engineering and Formal Methods. https:\/\/doi.org\/10.1007\/978-3-319-15201-1_1 10.1007\/978-3-319-15201-1_1","DOI":"10.1007\/978-3-319-15201-1_1"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-02217-3_5"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31374-5_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Sarah E. Chasins Elena L. Glassman and Joshua Sunshine. 2021. PL and HCI: Better Together. In Communications of the ACM. https:\/\/doi.org\/10.1145\/3469279 10.1145\/3469279","DOI":"10.1145\/3469279"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5075\/epfl-SYSTEMF-305144"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"\u0141 ukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. In Journal of Automated Reasoning. https:\/\/doi.org\/10.1007\/s10817-018-9458-4 10.1007\/s10817-018-9458-4","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_2_1_15_1","unstructured":"Manuel Eberl Gerwin Klein Peter Lammich Andreas Lochbihler Tobias Nipkow Larry Paulson Ren\u00e9 Thiemann and Dmitriy Traytel. 2004\u20132025. Archive of Formal Proofs. https:\/\/www.isa-afp.org\/"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/3563572.3563603"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639581"},{"key":"e_1_2_1_19_1","unstructured":"Georges Gonthier Assia Mahboubi and Enrico Tassi. 2016. A Small Scale Reflection Extension for the Coq System. Inria Saclay Ile de France. https:\/\/inria.hal.science\/inria-00258384"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591221"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Ben Greenman Sam Saarinen Tim Nelson and Shriram Krishnamurthi. 2023. Little Tricky Logic: Misconceptions in the Understanding of LTL. In The Art Science and Engineering of Programming. https:\/\/doi.org\/10.22152\/programming-journal.org\/2023\/7\/7 10.22152\/programming-journal.org\/2023\/7\/7","DOI":"10.22152\/programming-journal.org\/2023\/7\/7"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_23"},{"key":"e_1_2_1_23_1","volume-title":"Delve: Qualitative Data Analysis Software. https:\/\/delvetool.com\/","author":"Ho LaiYee","year":"2025","unstructured":"LaiYee Ho and Alex Limpaecher. 2025. Delve: Qualitative Data Analysis Software. https:\/\/delvetool.com\/"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2821566"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris From the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. In Journal of Functional Programming. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/985692.985712"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575671"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3643991.3644908"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485532"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070529"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2023.24"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the International Workshop on the Implementation of Logics. https:\/\/www.cl.cam.ac.uk\/~lp15\/papers\/Automation\/paar.pdf","author":"Lawrence","unstructured":"Lawrence C. Paulsson and Jasmin C. Blanchette. 2012. Three Years of Experience with Sledgehammer, A Practical Link between Automatic and Interactive Theorem Provers. In Proceedings of the International Workshop on the Implementation of Logics. https:\/\/www.cl.cam.ac.uk\/~lp15\/papers\/Automation\/paar.pdf"},{"key":"e_1_2_1_34_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u0103t\u0103lin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2024","unstructured":"Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u0103t\u0103lin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey. 2024. Logical Foundations (Software Foundations, Vol. 1). Electronic Textbook. http:\/\/softwarefoundations.cis.upenn.edu"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-43513-3_10"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3426425.3426940"},{"key":"e_1_2_1_37_1","unstructured":"Talia Ringer. 2020. Mechanized Proofs for PL: Past Present and Future. https:\/\/blog.sigplan.org\/2020\/01\/29\/mechanized-proofs-for-pl-past-present-and-future\/"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000045"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454033"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373823"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.26"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786855"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Jessica Shi Cassia Torczon Harrison Goldstein Benjamin C. Pierce and Andrew Head. 2025. Artifact for QED in Context: An Observation Study of Proof Assistant Users. https:\/\/doi.org\/10.5281\/zenodo.14942098 10.5281\/zenodo.14942098","DOI":"10.5281\/zenodo.14942098"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2404.12534"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2652524.2652551"},{"key":"e_1_2_1_46_1","unstructured":"Coq LSP Development Team. 2022\u20132025. Coq LSP. https:\/\/github.com\/ejgallego\/coq-lsp"},{"key":"e_1_2_1_47_1","unstructured":"HOL Development Team. 1988\u20132025. HOL Interactive Theorem Prover. https:\/\/hol-theorem-prover.org\/"},{"key":"e_1_2_1_48_1","unstructured":"Isabelle Development Team. 1994\u20132025. Isabelle. https:\/\/isabelle.in.tum.de\/"},{"key":"e_1_2_1_49_1","unstructured":"Lean Development Team. 2015\u20132025. Lean. https:\/\/lean-lang.org\/"},{"key":"e_1_2_1_50_1","unstructured":"Rocq Development Team. 1989\u20132025. The Rocq Prover. http:\/\/coq.inria.fr"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44043-8_28"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2310.18457"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.PLATEAU.2018.5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720426","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720426","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:14:02Z","timestamp":1760030042000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720426"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":53,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720426"],"URL":"https:\/\/doi.org\/10.1145\/3720426","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}