[chriswarbo]

"no NULL checks, no out of bounds checks"

You only need dynamic (run-time) checks to account for scenarios that the static (compile-time) checks couldn't rule out. For example, a Python programmer might use a run-time check to ensure a number is >= 0, but a C programmer can declare it as an unsigned int and not have to bother with that check.

In the same way, if we have a proof that, for all inputs, an index will never overflow an array, then we don't need a bounds check. Likewise for integer overflows, null pointers and any other assertion you like.

Proving a property holds for all inputs is more difficult than checking it holds for each input we are given, but the advantage is that in many situations a failed run-time check can be unrecoverable:

    missile.nose.onImpact = function(event) {
      switch (event.object) {
        case target:
          console.log('Hit!');
          missile.explode();
          break;

        case silo.door:
          // Should never get here...
          console.log('Oops!');
          break;

        default:
          console.log('Miss!');
          break;
      }
      
    };
    missile.fire();