How to show that this algorithm for evaluating polynomials works?
I suggest you use proof by induction, on the number of iterations of the loop.

In particular, find a loop invariant: an equation that relates the value of y, i, and $a_0,a_1,\dots,a_n$, and that always holds each time you reach the head of the loop.

Then, prove that your loop invariant is indeed an invariant, using proof by induction.