Consider predicate types, or first-class null safety through unions.

If statements introduce propositions, which type systems could take advantage.

example:

  let idx = randomInt();
  if (0 <= idx && idx < arr.length) { // proposition introduced
    // idx now has type: int where 0 <= idx && idx < arr.length
    // irrefutable proof of safe indexing by type propositions
    let value = arr[idx];
  }