Usability Barriers for Liquid Types (Summary of Published Work)
summary
Study of 19 developers (12 new to LiquidHaskell, 7 experienced) identifies nine concrete barriers across three themes: verification, developer experience, and scalability. Examples: SMT-backed proofs sometimes take five-hour verification runs and force commenting out code; the tool shows unhelpful SMT error messages with solver-introduced variables that don’t map to source locations; the language/spec boundary causes an unclear divide between code and specs so invariants live out of sight; installs fail easily, IDE support is sparse, and automation vs manual proof work remains brittle.
AI-written summary · about
chapters (11)
- 0:00Liquid types promise
- 1:46Why developers avoid liquid types
- 2:50Study design: new vs experienced users
- 5:20Usability barriers categories
- 6:23Verification challenges examples
- 9:10Error message challenges
- 11:17Installation and learning gaps
- 12:18SMT solver scalability
- 14:04Barriers beyond LiquidJava
- 16:11Improving usability in Liquid Java
- 17:33Q&A
related talks
34mLiquid Haskell: Verification with Refinement Types
58mLiquidHaskell: Liquid Types for Haskell
46mRefinement Types from Light to Deep Verification
01h 02mLanguage Design meets Verifying Compilers
53mSemantics-based program manipulation in the age of LLMs
21mRefinement Type Refutations
41mLiving inside a Theorem Proving Universe
20mFlux: Liquid Types for Rust