Spanning list reduction to basis & relation to Algorithm Correctness From the book "Linear Algebra Done Right" I noticed the proof for reduction of a spanning list in vector space is algorithmic:

Now, I'm convinced of this algorithm. But If I wanted to prove it, would proof-of-correctness of the algorithm suffice? ( since we have a loop [ represented as steps ], we can prove correctness by finding a loop invariant ).  Is proof by simple induction here ( on $ n $ ) is any different?
 A: I'm not sure if I understand what you're asking, but if you show that the algorithm does what it is supposed to do, namely reduce a spanning list to a basis, then that gives you a proof of the theorem. In fact, it gives you more, because it also tells you how to reduce a spanning set into a basis if you were actually given one.
That said, if you would want to implement the procedure outlined in the proof of the book into say a computer, then you might want to add some details on checking whether $v_j$ is in the span of $v_{0},\ldots,v_{j-1}$. For the purpose of the theoretical algorithm, this is somewhat irrelevant, because we know that it either is in the span, or it's not, and the algorithm will proceed either way.
Edit. Regarding the steps in the comment:
1 and 3. is verified at the end of the proof: using (2.21) it is observed that the output of the algorithm is indeed a basis. 2. is true because at each step $j$, you turn your attention to vector $v_j$, and since there are finitely many vectors, you will surely at some point reach the last vector. I do not understand 4. As for 5.: The proof gives no indication on how to implement the algorithm in practice, or how long it would take for a computer to finish it. In that sense, it might not be considered a true algorithm. In fact, let me rephrase 'Step $j$' as follows:

*

*Step $j$: Ask the Lord Almighty if $v_j$ is in the span of $v_1,\ldots,v_{j-1}$. If so, delete it; if not, leave it unchanged.

I claim that the proof is still valid when phrased in this rather crazy way. Indeed, all that matters is that there is an outcome to the step: either $v_j$ is in the span, or it's not. Whether a computer can actually figure that out is besides the point: there's an answer either way and you get to move on to step $j+1$ either way.
