That can't prevent every logic error. Here's[0] something I remember reading that really impressed me with static analysis tools. Running PVS-Studio against the Unreal 4 Engine (which is entirely C++).

It was able to detect a surprising number of logic errors, probably just caused by as tired programmer, or copy-pasting too quickly. For example in the function below, it was able to spot that the last 2 clauses of that comparison are identical. The programmer meant to use a '+' instead of '-' in the last one. I don't think you could have a type system that would disallow this logic error. (If it is possible, please prove me wrong, because that sounds awesome).

  static bool PositionIsInside(....)
  {
    return
      Position.X >= Control.Center.X - BoxSize.X * 0.5f &&
      Position.X <= Control.Center.X + BoxSize.X * 0.5f &&
      Position.Y >= Control.Center.Y - BoxSize.Y * 0.5f &&
      Position.Y >= Control.Center.Y - BoxSize.Y * 0.5f;
  }

[0] http://www.viva64.com/en/b/0249/