Usability Barriers for Liquid Types
Catarina Gamboa, Abigail Reese, Alcides Fonseca, Jonathan Aldrich
Abstract
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. 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.
• Human-centered computing → HCI design and evaluation methods.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 3ad8d6ac-4849-4ecd-baad-9de7912163adCited by top-tier papers3
- ROSpec: A Domain-Specific Language for ROS-Based Robot SoftwarePaulo Canelas, Bradley R. Schmerl, Alcides Fonseca, Christopher Steven TimperleyOOPSLA 2025 · 2 citations
- On the Impact of Formal Verification on Software DevelopmentEric Mugnier, Yuanyuan Zhou, Ranjit Jhala, Michael CoblenzOOPSLA 2025
- First-Class Refinement Types for ScalaMatt Bovel, Viktor Kunčak, Martin OderskyOOPSLA 2026
Builds on12
- Flux: Liquid Types for RustNico Lehmann, Adam T. Geller, Niki Vazou, Ranjit JhalaPLDI 2023 · 29 citations
- Learning and Programming Challenges of Rust: A Mixed-Methods StudyShuofei Zhu, Ziyi Zhang, Boqin Qin, Aiping Xiong et al.ICSE 2022 · 27 citations
- A Grounded Conceptual Model for Ownership Types in RustWill Crichton, Gavin Gray, Shriram KrishnamurthiOOPSLA 2023 · 25 citations
- STORM: Refinement Types for Secure Web ApplicationsNico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang et al.OSDI 2021 · 21 citations
- Property-Based Testing in PracticeHarrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce et al.ICSE 2024 · 21 citations
Related papers
- Usability-Oriented Design of Liquid Types for JavaCatarina Gamboa, Paulo Canelas, Christopher Steven Timperley, Alcides FonsecaICSE 2023 · 9 citations
- Quotient Haskell: Lightweight Quotient Types for AllBrandon Hewer, Graham HuttonPOPL 2024 · 3 citations
- Verifying replicated data types with typeclass refinements in Liquid HaskellYiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper et al.OOPSLA 2020 · 24 citations
- Liquidate your assets: reasoning about resource usage in liquid HaskellMartin A. T. Handley, Niki Vazou, Graham HuttonPOPL 2020 · 38 citations
- PLEX: Normalization for Refinement TypesAlessio Ferrarini, Niki Vazou, Wouter SwierstraOOPSLA 2026
