>>40Ah but you see, maths is not limited to execution of programs. An inductive argument from the algorithm's formal representation, and another relating it to its implementation, is sufficient to prove correctness of the algorithm and the program code. In practice we'd add tests to an arbitrary (small) subset of ∞, and some tool-driven coverage analysis.
That being said, the weight of that critique is on the case of the zero-element list. One might counter that it's appropriate to leave the average of nothing undefined, but thass' just some sloppy-ass whack right thur as far as pretending to do proper engineering goes.