> All dereference and array accesses must be statically verifyable, rather than causing sequenced exceptions This is such a pipe dream. In so many cases you w

> All dereference and array accesses must be statically verifyable, rather than causing sequenced exceptions This is such a pipe dream. In so many cases you will not be able to verify array index statically except by having the programmer write assert statements which the compiler could do automatically when it can't prove correctness (like the java JIT which can lift out bounds checking from loops).