Testing cannot ensure correctness, but verification can. The problem with a specify-and-verify approach is the first part: the specification. Programmers are often reluctant to write specifications because it seems like extra work, beyond writing the code.
In the context of pluggable type-checking, the specifications are annotations. Writing @Nullable annotations lets a verifier prove your program has no null pointer exceptions. Writing @MustCall andd @Owning lets a verifier prove your program has no resource leaks. And so forth.
Sometimes we can infer specifications from program executions or from code comments. An even better source is the source code itself. So far, writing a new type inference tool has been a big effort, which has to be re-done for each type system.
Help is on the way. Martin Kellogg, his students, and I have just published a paper, "Pluggable type inference for free" (in ASE 2023), that shows how to convert any type-checker into a type inference. In other words, every type-checker now has an accompanying type inference tool.
To build our tool, we observed that pluggable type systems already do local type inference (within a method). Our whole-program inference (called WPI) wraps a fixed-point loop around this. There are many complications beyond this idea, which you can read about in the paper.
In addition to being published in an academic conference, the technique is practical. It is distributed with the Checker Framework. This means that WPI has already created type inference tools for dozens of type systems, which you can use immediately.
The manual section on WPI tells you how to use it. You can get started by running the wpi.sh script, which automatically understands many Ant, Maven, and Gradle build files. Give it a try! We look forward to your comments, suggestions, and even your bug reports.
