Optional Type Systems for Java: Current Approaches and Ongoing Efforts
COM1 Level 3
MR1, COM1-03-19
Abstract:
The Java type system gives useful guarantees about software, but there are many properties that cannot be expressed. One pervasive property that cannot be expressed is whether a reference can be null or not. The resulting null pointer exceptions are the bane of programmers and have been called the “billion dollar mistake”. They happen even if you think hard about your code and test it thoroughly. There are many causes for null pointer exceptions, including object initialization, missing map keys, confusing contracts, and missing checks. There are many other properties that cannot be expressed in the Java type system that lead to severe runtime errors.
Optional type systems allow developers to improve the quality of their software by encoding additional properties as type systems and enforcing these properties at compile time. We will discuss a type system that prevents null pointer exceptions at compile time and the general framework it builds upon. These optional type systems have found hundreds of bugs in millions of lines of well-tested code. We will discuss alternative tools and interoperability, in particular with Kotlin, and the JSpecify effort to standardize static analysis annotations across the Java ecosystem. Finally, we will briefly discuss whole-program type inference and the interaction of optional type systems with deductive verification.
Bio:
Werner Dietl is an associate professor in Electrical and Computer Engineering at the University of Waterloo, Canada. His research interests are in safe and productive software development. He combines theoretical results with practical tools so developers can create high-quality, trustworthy software and reduce the enormous impact of software defects.
https://ece.uwaterloo.ca/~wdietl/