[justinpombrio]

A type system is sound when:

    for all expressions e:
      if e type checks with type t, then one of the following holds:
        - e evaluates to a value v of type t; or
        - e does not halt; or
        - e hits an "unavoidable error"
          like division by 0 or null deref
          (what counts as "unavoidable" varies from lang to lang)

Notice anything interesting about this definition? It uses the word "evaluate"! Type soundness is not just a statement about the type checker. It relates type checking to run time (and thus to compilation too). That is, if you muck with Java's runtime or compiler, you can break type soundness, even if you don't change its type system in the slightest.

[ukj]

Yes this is precisely what I am talking about.

Different implementations of eval() a.k.a different programming languages have different semantics.

Which implicit eval() implementation does the above hold?

What type system do you have in mind such that the above holds for ALL expressions. Type-checking itself is not always decidable.