[bjourne]

> This would be the case that I referred to in the second paragraph of my last comment. I would agree if we were talking about explicit type checks, but a portable Common Lisp program cannot consider implicit added by the compiler to be part of the programs semantics, because a compliant implementation is not required to add any type checks.

Hence if you want to talk about portable Common Lisp, you cannot achieve any type of soundness!

> This would be where our view is different. You consider soundness to be a guarantee given by the compiler, while I consider it a property of the program itself (which can sometimes be checked by the compiler, and sometimes by the programmer).

Your view is wrong. Read about type system soundness here https://papl.cs.brown.edu/2014/safety-soundness.html