paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Usability Barriers for Liquid Types

液体类型(Liquid Types)的可用性障碍
PLDI 9(PLDI)2025匹配度 2/10 · 论文研究 LiquidHaskell 的可用性障碍,属于液体类型与程序验证工具的人因研究,与用户核心关注的 LLM/Agent 结合静态分析、浮点程序分析、贝叶斯程序分析等方向没有直接交集。引用 3 inbox
Catarina Gamboa, Abigail Reese, Alcides Fonseca, Jonathan Aldrich
crossref: 2026-09-10

AI 速览

一句话:通过研究揭示 LiquidHaskell 开发者面临的九类可用性障碍,为液体类型系统设计提供依据。

液体类型(liquid types)能够表达比简单类型系统更丰富的验证性质,但至今仍未获得广泛采用。为理解其中原因,本文对开发者使用液体类型时所遇挑战进行了研究,重点关注 LiquidHaskell。研究识别出九项关键障碍,可归为三类:开发者体验、面对复杂与大型代码库时的可扩展性挑战,以及对验证过程的理解困难。这些发现综合呈现了阻碍液体类型更广泛采用的可用性问题,并为当前及未来液体类型系统的设计与实现提供启示。

问题
液体类型虽能表达比简单类型系统更丰富的验证性质,却未被广泛采用;论文旨在理解开发者使用液体类型时遇到的具体挑战及其原因。
方法
围绕 LiquidHaskell 开展可用性研究,分析开发者在采用和使用液体类型过程中面临的困难,并归纳这些障碍的类别。
评估
研究识别出三大类共九项关键障碍,涵盖开发者体验、复杂与大型代码库的可扩展性,以及对验证过程的理解,并据此提出对液体类型系统设计与实现的启示。
原文摘要(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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3145,
  title = {Usability Barriers for Liquid Types},
  author = {Catarina Gamboa and Abigail Reese and Alcides Fonseca and Jonathan Aldrich},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {PLDI},
  year = {2025},
  doi = {10.1145/3729327}
}