Liquid types extend traditional type systems with logical predicates that allow developers to express complex properties in different applications. For example, they have been used to track data between different layers in MVC applications in Haskell, model typestate protocols in Java, and track the semantics of database queries in Rust. Despite their expressive power and implementation in different languages, the general developer community has not yet adopted liquid types, which raises the question of the usability barriers to adopting and using liquid types.

In this paper, we present a study with 19 developers with different levels of expertise in using LiquidHaskell, the most mature implementation of liquid types now. Twelve developers were new to liquid types but familiar with the target language, while seven were experienced users who had used LiquidHaskell across different application areas. We used different qualitative research methods with these developers, including interviews, observations, retrospectives, and think-aloud protocols, depending on their expertise and the projects they could show us. This study identified nine barriers to adopting liquid types, spanning three themes: developer experience, scalability challenges with complex and large codebases, and understanding the verification process.

Verification barriers come from the unclear divide between the verification layer and the programming language, confusing verification features in liquid types, and the lack of familiarity with proof engineering. These challenges make it difficult for developers without a formal verification background to understand the verification process and how to use it effectively. The developer experience barriers compound the difficulties in understanding the verification process, since there is limited IDE support and learning resources, and the error messages can be unhelpful in diagnosing the problems. Setting up and installing the tools are also challenges that prevent developers from even starting to use liquid types. Finally, scalability challenges arise when working with large and complex codebases, where the verification often becomes slow, and internally, the SMT solver has limitations for certain types of properties. Additionally, the mix of automation and manual flexibility and the opaque use of the SMT solver make developers unsure of what is necessary to prove properties. The barriers identified in this study can also be seen in other implementations of liquid types and even other verification techniques. Therefore, by addressing these usability barriers, we can enable more developers to adopt these techniques and create more robust and reliable software.

This paper was recently published at PLDI 2025 (https://dl.acm.org/doi/10.1145/3729327) and brings together topics on programming languages, software engineering, and human-computer interaction to create a comprehensive view of the usability challenges to the broader adoption of liquid types.