The main hack done to the compiler is that generated code avoids certain constructs that inhibit perfect static analysis, allowing the NaCL host (i.e. Google Chrome at present) to verify the behaviour of some untrusted binary before ever executing it (just like Java does).
I am having a hard time with this. At first I thought this amounted to a claim that the halting problem had been solved, or else that Java and NaCl are not Turing complete. I'm guessing the problem is with the term "perfect." So something interesting must be going on or it wouldn't be worth mentioning. What's being verified? That the code can't execute data and won't call certain interrupts, or is something more interesting happening?
At first I thought this amounted to a claim that the halting problem had been solved,
That's not what the halting problem means! There is no rule that says you cannot prove a program is safe: the rule is only that you cannot prove any arbitrary program is safe. NaCl gets around that by adding checks to the code (bounds checks, etc) to anywhere that it can't prove is safe.
It's still Turing complete because it can perform arbitary computation; it just can't cause arbitrary behavior at the machine code level. (Indeed, making a VM that's both Turing complete and safe is not generally a hard problem - for example, most Brainfuck interpreters qualify. The hard problems are making safe interfaces to the rest of the system, and speed.)
I don't know exactly what NaCL does, but the JVM/CLR verification is all about making sure you don't write over someone else's memory, jump to some arbitrary address, etc. Essentially the problem is: how do you run untrusted code in the same address space, without it getting all of your process's permissions.
Halting problem is literally that the program will halt. That's not provable, even if you offer it on rentacoder.com.
JVM bytecode, .NET CLR bytecode, NACL bytecode are all verified as containing no illegal API calls. That's completely different. And its completely possible.
It doesn't have to solve the halting problem, just contain the code from interacting with the wider system except through tightly-defined interfaces. "does this code make any far jumps" is an answerable question when you can constrain the machine code generated and ban self-modifying code.
I am having a hard time with this. At first I thought this amounted to a claim that the halting problem had been solved, or else that Java and NaCl are not Turing complete. I'm guessing the problem is with the term "perfect." So something interesting must be going on or it wouldn't be worth mentioning. What's being verified? That the code can't execute data and won't call certain interrupts, or is something more interesting happening?