> I don't see anything in the WP article about proofs of correctness. "Finite sequence" surely just means that the number of instructions isn't infinite?

Well how are you going to show that the algorithm terminates for all inputs without a proof of correctness?