{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:14:25Z","timestamp":1760044465424,"version":"3.41.2"},"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' challenges with liquid types, focusing on LiquidHaskell.  \nOur 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":2,"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"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9971-8499","authenticated-orcid":false,"given":"Abigail","family":"Reese","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0879-4015","authenticated-orcid":false,"given":"Alcides","family":"Fonseca","sequence":"additional","affiliation":[{"name":"University of Lisbon, Lisbon, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0631-5591","authenticated-orcid":false,"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1080\/0142159X.2023.2289847"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3344429.3372508"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3287324.3287432"},{"key":"e_1_2_2_4_1","first-page":"G12","volume-title":"Evaluating the Usability of Interactive Verification Systems. In International Workshop on Comparative Empirical Evaluation of Reasoning Systems. 873","author":"Beckert Bernhard","year":"2012","unstructured":"Bernhard Beckert and Sarah Grebing. 2012. Evaluating the Usability of Interactive Verification Systems. In International Workshop on Comparative Empirical Evaluation of Reasoning Systems. 873, CEUR-WS.org, 3\u201317. https:\/\/dblp.org\/rec\/conf\/cade\/BeckertG12.bib"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622812"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.6092\/ISSN.1972-5787\/4593"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_10_1","unstructured":"Chris Brown. 2022. Nudging developers to participate in SE research. https:\/\/api.semanticscholar.org\/CorpusID:252539209"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775052.2661091"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115653"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3469279"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_2_2_15_1","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_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428200"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452379"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.52"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622841"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5381\/JOT.2006.5.5.A3"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3587157"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_23_1","unstructured":"Gilles Dowek Amy Felty Hugo Herbelin G\u00e9rard Huet Chetan Murthy Catherin Parent Christine Paulin-Mohring and Benjamin Werner. 1992. The COQ Proof Assistant: User\u2019s Guide: Version 5.6. INRIA."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1515\/comp-2019-0001"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5657.001.0001"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58115-2_2"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPC58990.2023.00029"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00132"},{"key":"e_1_2_2_30_1","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 Artifact containing research materials for the qualitative study on developer experiences with LiquidHaskell 10.5281\/zenodo.15044759","DOI":"10.5281\/zenodo.15044759"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607837"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639581"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1006\/JVLC.1996.0009"},{"volume-title":"Contextual Design","author":"Holtzblatt Karen","key":"e_1_2_2_35_1","unstructured":"Karen Holtzblatt and Hugh Beyer. 2016. Contextual Design, Second Edition: Design for Life (2nd ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA. isbn:0128008946"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_2_2_37_1","volume-title":"International Conference on Program Comprehension, ICPC, https:\/\/sarajuhosova.com\/assets\/files\/2025-icpc.pdf Accepted","author":"Juho\u0161ov\u00e1 S\u00e1ra","year":"2025","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, https:\/\/sarajuhosova.com\/assets\/files\/2025-icpc.pdf Accepted"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46982-9_7"},{"key":"e_1_2_2_39_1","volume-title":"Formal Underpinnings of Java Workshop (at OOPSLA\u201998)","author":"Leavens Gary T","year":"1998","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). 404\u2013420. https:\/\/citeseerx.ist.psu.edu\/document?repid=rep1&type=pdf&doi=397cb3c2ad6569aef081c282671d17937df483d0"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_2_2_41_1","volume-title":"STORM: Refinement Types for Secure Web Applications. In Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association, 441\u2013459","author":"Lehmann Nico","year":"2021","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. In Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association, 441\u2013459. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/lehmann"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704885"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485532"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048237.2048241"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509515"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2016.200"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.90"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001489"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-43513-3_10"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/227614.227615"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_59"},{"key":"e_1_2_2_53_1","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\u2013169. https:\/\/doi.org\/10.1145\/1375581.1375602 10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"volume-title":"The Coding Manual for Qualitative Researchers","author":"Salda\u00f1a Johnny","key":"e_1_2_2_54_1","unstructured":"Johnny Salda\u00f1a. 2009. The Coding Manual for Qualitative Researchers. SAGE Publications. isbn:978-1-84787-548-8"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1155\/2010\/602570"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689745"},{"key":"e_1_2_2_58_1","volume-title":"Introduction to Human Factors Engineering","author":"Wickens Christopher D.","year":"1837","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. isbn:0131837362","edition":"2"},{"key":"e_1_2_2_59_1","volume-title":"Titus Delafayette Winters, and Tom Manshreck","author":"Wright Hyrum","year":"2020","unstructured":"Hyrum Wright, Titus Delafayette Winters, and Tom Manshreck. 2020. Software Engineering at Google. O\u2019Reilly Media, Inc.. isbn:9781492082798"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10664-021-10003-7"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632910"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","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":[[2025,7,16]],"date-time":"2025-07-16T06:06:38Z","timestamp":1752645998000},"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":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}