Shortly after Java 6 came out last year, there were a number of Java 7 wish lists floating around (example). Most wishes are for syntax improvements. I don’t use Java as much as I used to, and I only have one wish list item: *static analysis optimizations*. That is, optimizations made possible with the help of static (not run-time) optimizations.

I’ve written before on the promising range check elimination optimization which strives to eliminate array bounds checking when provably unnecessary. But that optimization doesn’t quite live up to its potential because any nontrivial array usage is beyond the scope of a run-time proof. So the idea of static analysis optimization is for a compile-time (or post-compile-time) process to do an in-depth analysis of array usage and other potential optimizations and insert the suggested optimization and finished proof into the byte-code. Then the JVM only needs to verify the proof at run-time rather that construct a proof from scratch. And for that matter, the JVM could never generate a proof, since it could assume that if there is no proof provided already, there’s no use looking for one at run-time.

My motivation is scientific computing (especially linear algebra), which still seems to be unnecessarily handicapped in Java.

Very interesting. As you say a proof has to be provided and the JVM will need to verify it. Is the proof’s formal verification faster than its construction?

I would expect so — the hard part has got to be knowing where to look. At best, it’s like factorization, where finding factors for a large number is much harder than verifying a given factorization. At worst, you at least prevent the JVM from investigating dead ends.