Usability Barriers for Liquid Types
summary
Study reports a user study of LiquidHaskell with 12 novice and several experienced participants, yielding nine barriers across three concrete categories: verification, developer experience, and scalability. Findings include confusing verification features (measures and lifting), error messages that reference internal names, specs written as comments that feel optional, fragile IDE and install support, and SMT-driven verification that can take five hours or more. Exercises (a rotate invariant) exceed 30 minutes for novices and force code changes to satisfy the verifier.
AI-written summary · about
chapters (8)
- 0:00Liquid types introduction
- 2:07Study design
- 4:57Verification challenges
- 8:09Developer experience
- 10:40Scalability limits
- 12:04Generalizing barriers
- 13:29Future directions
- 13:51Q&A
related talks
29mIntegrating Liquid Haskell with GHC
23mHow Novices Perceive Interactive Theorem Provers (Extended Abstract)
43mVisual-textual functional programming with Luna
29mType Inference Techniques: Implementation and Formalization, Better Together
01h 26mHaskell Language Server
20mGetting into the Flow: Towards Better Type Error Messages for Constraint-Based ...
15mOn the Impact of Formal Verification on Software Development
25mLeveraging (algebraic data) types to make your UI rock solid