What's the difference between proving weak normalization and implementing evaluator?
If you implement an evaluator for the terms of a language $A$ in a total system $B$, and you have furthermore proven that your evaluator is correct, that is for every $t$ well-typed in $A$,

$$\mathrm{eval}(t) \simeq_A t $$

where $\simeq_A$ is the equality in $A$, then you have only shown that $\simeq_A$ is decidable.

If furthermore $\simeq_A$ naturally leads to a notion of reduction $\rightarrow_A$, and $\mathrm{eval}(t)$ is always in normal form, then you have proven that every term $t$ in $A$ is equivalent to a term in normal form.

This is enough for consistency of $A$ but is not equivalent to weak normalization, unless $\rightarrow_A$ is furthermore church-rosser!

This is essentially the approach taken by normalization by evaluation.

A proof of weak normalization in a constructive logic naturally leads to an evaluator, as every $\forall\exists$ statement leads to an algorithm (correct by construction).

There is a nice article by Ulrich Berger, Program extraction from normalization proofs, which implements this idea for simply typed $\lambda$-calculus.



For your second question, here is a counter example. Consider the language $A$ to have only two terms, $\Delta$ and $\bot$, with the reduction rules

$$\Delta\rightarrow \Delta $$
$$\Delta\rightarrow \bot $$

Feel free to add types if you like. The computation rules are weakly normalizing and confluent.

In Coq, you might write the eval function thus:

Fixpoint eval (t : A) : A :=
  match t with
     | Delta =&gt; Bottom
     | Bottom =&gt; Bottom


It's not too hard to prove that if $t\leftrightarrow^* u$ then eval(t) = eval(u). Coq's reduction can be taken to be non-deterministic, in which case you have a counter-example to the SN "inheritance" that you expect.