Usability-Oriented Design of Liquid Types for Java

Developers want to detect bugs as early in the development lifecycle as possible, as the effort and cost to fix them increases with the incremental development of features. Ultimately, bugs that are only found in production can have catastrophic consequences. Type systems are effective at detecting many classes of bugs during development, often providing immediate feedback both at compile-time and while typing due to editor integration. Unfortunately, more powerful static and dynamic analysis tools do not have the same success due to providing false positives, not being immediate, or not being integrated into the language. Liquid Types extend the language type system with predicates, augmenting the classes of bugs that the compiler or IDE can catch compared to the simpler type systems available in mainstream programming languages. However, previous implementations of Liquid Types have not used human-centered methods for designing or evaluating their extensions. Therefore, this paper investigates how Liquid Types can be integrated into a mainstream programming language, Java, by proposing a new design that aims to lower the barriers to entry and adapts to problems that Java developers commonly encounter at runtime. Following a participatory design methodology, we conducted a developer survey to design the syntax of LiquidJava, our prototype. To evaluate if the added effort to writing Liquid Types in Java would convince users to adopt them, we conducted a user study with 30 Java developers. The results show that LiquidJava helped users detect and fix more bugs and that Liquid Types are easy to interpret and learn with few resources. At the end of the study, all users reported interest in adopting LiquidJava for their projects.