> 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).
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