> Future-tech, remember.
Not so much future tech. The most sophisticated JIT in production use nowadays is HotSpot's optimizing JIT, and next year it's getting this: http://openjdk.java.net/jeps/165 (basically, metadata that the programmer can use to help the JIT with some decisions). HotSpot's next-gen JIT, Graal, takes five more steps forward and allow a full programmer-controlled JITting, that can suggest and improve various speculations on the semantic AST: https://wiki.openjdk.java.net/display/Graal/Publications+and...
I have full confidence in the general utility of JITs for server-side applications, but JITs themselves are a tradeoff (require warmup or caching, more RAM and more energy).
> There's nothing stopping you from transforming C code into Rust code
Not really, because Rust requires manual type annotations. Either they are added manually -- in which case you may as well translate manually -- or automatically, in which case the tranlator would need to infer the very same properties you want to verify.
> Just that language semantics (which consist of such things as a type system, a threading/memory model, etc.) have no reason to be tied to either a particular syntax, or a particular VM.
But they do because it's not just syntax -- the language and runtime are really a part of the algorithm (in fact, most algorithms presuppose a certain execution context like random, constant-time access to memory). The threading/memory model is what determines whether certain algorithms can be implemented at all; functional purity can completely change the complexity (by more than a constant) etc.
> I foresee much more of this, and much more cleverness about it: writing code that compiles to a bunch of separate modules for separate VMs, which then form a micro-distributed-system all within a Docker container or somesuch.
The problem with that is that once you go distributed (even on the same machine) there are tremendous performance costs involved. Not only marshalling/demarshalling of data, but fanning-in and then fanning out your concurrency on each end. There's no way you can use, say, a Java parallel stream, whose parallel operation is performed over the wire. There are only very specific places where you can place that boundary.
I do, however, think that a platform such as OpenJDK, with such powerful GCs and JITs, can -- and indeed does -- contribute significantly to the ability to interoperate among various languages -- but certainly not all of them.