LiquidJava:Catch Bugs at Compile Time with Liquid Types
summary
LiquidJava extends Java types with refinement predicates so the compiler proves properties like “height > 0” and object protocol states (cannot write after close) using an SMT solver, a research prototype implementation and a VS Code extension. Live demos show it finds real defects (a StackOverflow example) and it already surfaces two bugs found in open-source projects. Verification is fast on small modules and supports modular rechecking, but it lacks concurrency/randomized-value reasoning, and hasn’t been validated on large enterprise codebases or Kotlin/IntelliJ workflows.
AI-written summary · about
chapters (10)
- 0:00Introduction to LiquidJava
- 1:50How Liquid Types Work
- 3:15Simple Refinement Examples
- 4:38Refining Methods and Returns
- 7:09Object Protocols for Sockets
- 9:35Debugging the First Bug
- 11:46Real-World Use Cases
- 13:50Future of LiquidJava
- 15:13Call to Action and Feedback
- 16:49Q&A Session
related talks
15mWell-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers
01h 20mGrowing the Java Language
14mTypeless Writing in a Strong Typed World
36mRetrofitting Null-Safety into Java
01h 00mJava Language Futures - All Aboard Project Amber
58mDebugging #Java
23mThe Java Features You’re Missing Out On
56mJava Sucks (So C# Didn't Have To)