What's the difference between proving weak normalization and implementing evaluator? Implementing an normalization (cut elimination) procedure for a type system A in a language with a total type system B, automatically proves cut elimination for type system A since the implementation will be total.

What's the difference between proving weak normalization and implementing the evaluator?

If there is none, is that effect also present in proving consistency of all the mathematical proof systems?

The same question in a strong normalization setting:
If the host language is strongly normalizing does strong normalization of client language follows?
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.