Prove correctness of the iterative algorithm
Let Nums be the value of the array after method execution,
and nums the initial value. Let,

P(i) = Nums[0..i-1] is the same as nums[0..i-1], but ignoring `val`.


Your algorithm is correct if P(nums.length) is true.
This can be shown by realising that P is true at the beginning
of the loop, and each iteration of the loop preserves P.

Initially, i = 0 in the for loop, and we have

   P(0)
 = Nums[0..0-1] is the same as nums[], but ignoring `val`.
 = Nums[] is the same as nums[], but ignoring `val`.
 = true


Next, assuming P(i), for $i \leq nums.length$, show P(i+1) ;-)



This is some of the work of the Hoare Calculus mentioned above.