{"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":1785381755540,"version":"3.55.0"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"name":"Portuguese Foundation for Science and Technology through the Carnegie Mellon Portugal Program","award":["RT\/BD\/154254\/2021"],"award-info":[{"award-number":["RT\/BD\/154254\/2021"]}]},{"name":"Portuguese Foundation for Science and Technology through LASIGE Research Unit","award":["UID\/00408\/2025"],"award-info":[{"award-number":["UID\/00408\/2025"]}]},{"name":"Portuguese Foundation for Science and Technology through the RAP project","award":["(https:\/\/doi.org\/10.54499\/EXPL\/CCI-COM\/1306\/2021"],"award-info":[{"award-number":["(https:\/\/doi.org\/10.54499\/EXPL\/CCI-COM\/1306\/2021"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>Liquid types can express richer verification properties than simple type systems. However, despite their advantages, liquid types have yet to achieve widespread adoption. To understand why, we conducted a study analyzing developers\u2019 challenges with liquid types, focusing on LiquidHaskell. Our findings reveal nine key barriers that span three categories, including developer experience, scalability challenges with complex and large codebases, and understanding the verification process. Together, these obstacles provide a comprehensive view of the usability challenges to the broader adoption of liquid types and offer insights that can inform the current and future design and implementation of liquid type systems.<\/jats:p>","DOI":"10.1145\/3729327","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1911-1936","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Usability Barriers for Liquid Types"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6995-7340","authenticated-orcid":false,"given":"Catarina","family":"Gamboa","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"},{"name":"University of Lisbon, Lisbon, Portugal"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9971-8499","authenticated-orcid":false,"given":"Abigail","family":"Reese","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0879-4015","authenticated-orcid":false,"given":"Alcides","family":"Fonseca","sequence":"additional","affiliation":[{"name":"University of Lisbon, Lisbon, Portugal"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0631-5591","authenticated-orcid":false,"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1080\/0142159X.2023.2289847"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Brett A. Becker Paul Denny Raymond Pettit Durell Bouchard Dennis J. Bouvier Brian Harrington Amir Kamil Amey Karkare Chris McDonald Peter-Michael Osera Janice L. Pearce and James Prather. 2019. Compiler Error Messages Considered Unhelpful: The Landscape of Text-Based Programming Error Message Research. In Working Group Reports on Innovation and Technology in Computer Science Education ITiCSE-WGR. ACM 177-210. https:\/\/doi.org\/10.1145\/3344429.3372508 10.1145\/3344429.3372508","DOI":"10.1145\/3344429.3372508"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Brett A. Becker and Keith Quille. 2019. 50 Years of CS1 at SIGCSE: A Review of the Evolution of Introductory Programming Education Research. In Technical Symposium on Computer Science Education (Minneapolis MN USA) (SIGCSE \u201919). ACM 338-344. https:\/\/doi.org\/10.1145\/3287324.3287432 10.1145\/3287324.3287432","DOI":"10.1145\/3287324.3287432"},{"key":"e_1_3_2_5_2","unstructured":"Bernhard Beckert and Sarah Grebing. 2012. Evaluating the Usability of Interactive Verification Systems. In International Workshop on Comparative Empirical Evaluation of Reasoning Systems Vol. 873. CEUR-WS.org 3-17. https:\/\/db1p.org\/.rec\/conf\/cade\/BeckertG12.bib"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622812"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.6092\/ISSN.1972-5787\/4593"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","unstructured":"Ana Bove Peter Dybjer and Ulf Norell. 2009. A brief overview of Agda a functional language with dependent types. In International Conference on Theorem Proving in Higher Order Logics. Springer 73-78.","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_11_2","unstructured":"Chris Brown. 2022. Nudging developers to participate in SE research. https:\/\/api.semanticscholar.org\/CorpusID:252539209"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775052.2661091"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Carl Chapman Peipei Wang and Kathryn T. Stolee. 2017. Exploring regular expression comprehension. In International Conference on Automated Software Engineering (ASE). IEEE Computer Society 405-416. https:\/\/doi.org\/10.1109\/ASE.2017.8115653 10.1109\/ASE.2017.8115653","DOI":"10.1109\/ASE.2017.8115653"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3469279"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Ravi Chugh David Herman and Ranjit Jhala. 2012. Dependent types for JavaScript. Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA). ACM 587-606. https:\/\/doi.org\/10.1145\/2384616.2384659 10.1145\/2384616.2384659","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Michael Coblenz April Porter Varun Das Teja Nallagorla and Michael Hicks. 2023. A Multimodal Study of Challenges Using Rust. https:\/\/doi.org\/10.1184\/R1\/22277326.v1 10.1184\/R1\/22277326.v1","DOI":"10.1184\/R1\/22277326.v1"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428200"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3452379"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Michael J. Coblenz Whitney Nelson Jonathan Aldrich Brad A. Myers and Joshua Sunshine. 2017. Glacier: transitive class immutability for Java. International Conference on Software Engineering (ICSE). IEEE \/ ACM 496-506. https:\/\/doi.org\/10.1109\/ICSE.2017.52 10.1109\/ICSE.2017.52","DOI":"10.1109\/ICSE.2017.52"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622841"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.5381\/JOT.2006.5.5.A3"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3587157"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner. 2008. Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science Vol. 4963). Springer 337-340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_24_2","unstructured":"Gilles Dowek Amy Felty Hugo Herbelin G\u00e9rard Huet Chetan Murthy Catherine Parent Christine Paulin-Mohring and Benjamin Werner. 1992. The COQ Proof Assistant: User\u2019s Guide: Version 5.6. INRIA."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1515\/comp-2019-0001"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5657.001.0001"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3 - Where Programs Meet Provers. In Programming Languages and Systems - ESOP (LNCS Vol. 7792). Springer 125-128. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8 10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Alcides Fonseca Paulo Santos and Sara Silva. 2020. The Usability Argument for Refinement Typed Genetic Programming. In Parallel Problem Solving from Nature - PPSN (LNCS Vol. 12270). Springer 18-32. https:\/\/doi.org\/10.1007\/978-3-030-58115-2_2 10.1007\/978-3-030-58115-2_2","DOI":"10.1007\/978-3-030-58115-2_2"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Shuai Fu Tim Dwyer Peter J. Stuckey Jackson Wain and Jesse Linossier. 2023. ChameleonIDE: Untangling Type Errors Through Interactive Visualization and Exploration. In International Conference on Program Comprehension (ICPC). IEEE 146-156. https:\/\/doi.org\/10.1109\/ICPC58990.2023.00029 10.1109\/ICPC58990.2023.00029","DOI":"10.1109\/ICPC58990.2023.00029"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Catarina Gamboa Paulo Canelas Christopher Steven Timperley and Alcides Fonseca. 2023. Usability-Oriented Design of Liquid Types for Java. International Conference on Software Engineering (ICSE). IEEE 1520-1532. https:\/\/doi.org\/10.1109\/ICSE48619.2023.0013210.1109\/ICSE48619.2023.00132","DOI":"10.1109\/ICSE48619.2023.00132"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Catarina Gamboa Abigail Reese Alcides Fonseca and Jonathan Aldrich. 2025. Artifact for \"Usability Barriers for Liquid Types\". Zenodo repository. https:\/\/doi.org\/10.5281\/zenodo.15044759 10.5281\/zenodo.15044759 Artifact containing research materials for the qualitative study on developer experiences with LiquidHaskell.","DOI":"10.5281\/zenodo.15044759"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Hubert Garavel Maurice H. ter Beek and Jaco van de Pol. 2020. The 2020 Expert Survey on Formal Methods. Formal Methods for Industrial Critical Systems (FMICS) (Vienna Austria). Springer 3-69. https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1 10.1007\/978-3-030-58298-2_1","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607837"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Harrison Goldstein Joseph W. Cutler Daniel Dickstein Benjamin C. Pierce and Andrew Head. 2024. Property-Based Testing in Practice. In International Conference on Software Engineering (ICSE) (Lisbon Portugal). Association for Computing Machinery Article 187 13 pages. https:\/\/doi.org\/10.1145\/3597503.3639581 10.1145\/3597503.3639581.","DOI":"10.1145\/3597503.3639581"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1006\/JVLC.1996.0009"},{"key":"e_1_3_2_36_2","unstructured":"Karen Holtzblatt and Hugh Beyer. 2016. Contextual Design Second Edition: Design for Life (2nd ed.). Morgan Kaufmann Publishers Inc. San Francisco CA USA."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","unstructured":"S\u00e1ra Juho\u0161ov\u00e1 Andy Zaidman and Jesper Cockx. 2025. Pinpointing the Learning Obstacles of an Interactive Theorem Prover. International Conference on Program Comprehension (ICPC) (2025) https:\/\/sarajuhosova.com\/assets\/files\/2025-icpc.pdf Accepted.","DOI":"10.1109\/ICPC66645.2025.00024"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Nikolai Kosmatov and Julien Signoles. 2016. Frama-C A Collaborative Framework for C Code Verification: Tutorial Synopsis. In Runtime Verification (RV) (Lecture Notes in Computer Science Vol. 10012). Springer 92-115. https:\/\/doi.org\/10.1007\/978-3-319-46982-9_7 10.1007\/978-3-319-46982-9_7","DOI":"10.1007\/978-3-319-46982-9_7"},{"key":"e_1_3_2_40_2","unstructured":"Gary T. Leavens Albert L. Baker and Clyde Ruby. 1998. JML: a Java modeling language. In Formal Underpinnings of Java Workshop ( at OOPSLA\u201998).Citeseer 404-420. https:\/\/citeseerx.ist.psu.edu\/document?repid=rep1&type=pdf&doi=397cb3c2ad6569aef081c282671d17937df483d0."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_2_42_2","unstructured":"Nico Lehmann Rose Kunkel Jordan Brown Jean Yang Niki Vazou Nadia Polikarpova Deian Stefan and Ranjit Jhala. 2021. STORM: Refinement Types for Secure Web Applications. Operating Systems Design and Implementation (OSDI). USENIX Association 441-459. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/lehmann."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704885"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming Artificial Intelligence and Reasoning (Lecture Notes in Computer Science Vol. 6355). Springer 348-370. https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485532"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Guillaume Marceau Kathi Fisler and Shriram Krishnamurthi. 2011. Mind your language: on novices\u2019 interactions with error messages. In Symposium on New ideas New Paradigms and Reflections on Programming and Software (Portland Oregon USA) (Onward! 2011). ACM 3-18. https:\/\/doi.org\/10.1145\/2048237.2048241 10.1145\/2048237.2048241","DOI":"10.1145\/2048237.2048241"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Leo A. Meyerovich and Ariel S. Rabkin. 2013. Empirical analysis of programming language adoption. In International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA) Antony L. Hosking Patrick Th.Eugster and Cristina V. Lopes (Eds.). ACM 1-18. https:\/\/doi.org\/10.1145\/2509136.2509515 10.1145\/2509136.2509515","DOI":"10.1145\/2509136.2509515"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2016.200"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"Sebastian Nanz and Carlo A. Furia. 2015. A Comparative Study of Programming Languages in Rosetta Code. In International Conference on Software Engineering (ICSE). IEEE Computer Society 778-788. https:\/\/doi.org\/10.1109\/ICSE.2015.90 10.1109\/ICSE.2015.90","DOI":"10.1109\/ICSE.2015.90"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001489"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"Bartosz Piotrowski Ramon Fern\u00e1ndez Mir and Edward W. Ayers. 2023. Machine-Learned Premise Selection for Lean. In Automated Reasoning with Analytic Tableaux and Related Methods TABLEAUX 2023 (Lecture Notes in Computer Science Vol. 14278). Springer 175-186. https:\/\/doi.org\/10.1007\/978-3-031-43513-3_10 10.1007\/978-3-031-43513-3_10","DOI":"10.1007\/978-3-031-43513-3_10"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/227614.227615"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Patrick Maxim Rondon Alexander Bakst Ming Kawaguchi and Ranjit Jhala. 2012. CSolve: Verifying C with Liquid Types. In Computer Aided Verification (CAV) (Lecture Notes in Computer Science Vol. 7358). Springer 744-750. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_59 10.1007\/978-3-642-31424-7_59","DOI":"10.1007\/978-3-642-31424-7_59"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","unstructured":"Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In Programming Language Design and Implementation (PLDI). ACM 159-169. https:\/\/doi.org\/10.1145\/1375581.1375602 10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_55_2","unstructured":"Johnny Salda\u00f1a. 2009. The Coding Manual for Qualitative Researchers. SAGE Publications."},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","unstructured":"V. Javier Traver. 2010. On Compiler Error Messages: What They Say and What They Mean. Adv. Hum. Comput. Interact. 2010 (2010) 602570:1-602570:26. https:\/\/doi.org\/10.1155\/2010\/602570 10.1155\/2010\/602570","DOI":"10.1155\/2010\/602570"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","unstructured":"Niki Vazou Eric L. Seidel and Ranjit Jhala. 2014. LiquidHaskell: experience with refinement types in the real world. In ACM SIGPLAN Symposium on Haskell. ACM 39-51. https:\/\/doi.org\/10.1145\/2633357.2633366 10.1145\/2633357.2633366","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689745"},{"key":"e_1_3_2_59_2","unstructured":"Christopher D. Wickens John Lee Yili D. Liu and Sallie Gordon-Becker. 2003. Introduction to Human Factors Engineering (2nd Edition). Prentice-Hall Inc. USA."},{"key":"e_1_3_2_60_2","unstructured":"Hyrum Wright Titus Delafayette Winters and Tom Manshreck. 2020. Software Engineering at Google. O\u2019Reilly Media Inc."},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10664-021-10003-7"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632910"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","unstructured":"Shuofei Zhu Ziyi Zhang Boqin Qin Aiping Xiong and Linhai Song. 2022. Learning and programming challenges of rust: a mixed-methods study. International Conference on Software Engineering ICSE (Pittsburgh Pennsylvania). ACM 1269-1281. https:\/\/doi.org\/10.1145\/3510003.3510164 10.1145\/3510003.3510164","DOI":"10.1145\/3510003.3510164"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729327","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:06:43Z","timestamp":1784196403000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729327"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":62,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729327"],"URL":"https:\/\/doi.org\/10.1145\/3729327","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}