Well, I don't consider an OS or a browser to be the implementation of an algorithm. It has to be possible to understand an algorithm, re-implement it, and so on. I'd say you have to be able to hold it in your head - like Eratosthenes' Sieve.

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? Come to think of it, that wording seems rather hand-wavey; I wonder if I can find citations to help me improve it.