[juki]

We must be using a different definition of soundness then. As I see it, implicit run time type checks do not affect the semantics of a program, and as such, do not have any bearing on its soundness. They're merely a debugging tool to help one detect unsoundness as early as possible in development, or to fail gracefully with good error logging in a production environment. Optimizing for `(safety 0)` only tells the compiler that you know the piece of code is sound, so there is no need to check at run time. It's still just as sound or unsound as it would be with the type checks.

I suppose you could argue that someone might write a program that relies on being able to call a function with the wrong type of arguments and catch the resulting error. In this case removing the type checks obviously changes the behavior of the program. This however would not be portable across different CL implementations anyway, so you should really be using explicit type checks.

> But the difference is the frequency in which it is lost. In SBCL Lisp, if you want fast code, the answer is "almost all the time".

SBCL code is fast enough for the vast majority of a program even with full run time type checking, so you would only be using `(safety 0)` for very performance critical code, whose safety you have ensured yourself. The `(safety 0)` declaration also does not disable any compile time checking that SBCL does.

[bjourne]

Run time type checks affects the semantics of programs. Consider an identity function declared to only accept fixnums and returns fixnums. If you call this function with a string a type error will be signaled if run time type checks are enabled. This is sound. If you call this function with a string without run time type checks the function will return the string it got in. This is not sound because the run time thinks that it has a fixnum while in reality it is a string. The likely consequence is a segfault.

Think of soundness as a guarantee that if the program type checks, then all type declarations are correct. Note also that soundness is a property of the type system itself. A piece of code is not sound or unsound -- it is the type system itself that is.

[lispm]

SBCL is a strange Lisp implementation, since it does some compile-time type checks, too.

  * (defun id (f) f)
  ID
  * (declaim (ftype (function (fixnum) fixnum) id))
  (ID)

Our new identity function is declared to be of type fixnum -> fixnum.

  * (declaim (optimize (safety 0)))
  NIL

Now we've set safety to 0.

Let's define a function which calls ID with a string

  * (defun use-id (s) (declare (type string s)) (id s))
  ; in: DEFUN USE-ID
  ;     (ID S)
  ; 
  ; caught WARNING:
  ;   Derived type of S is
  ;     (VALUES STRING &OPTIONAL),
  ;   conflicting with its asserted type
  ;     FIXNUM.
  ;   See also:
  ;     The SBCL Manual, Node "Handling of Types"
  ; 
  ; compilation unit finished
  ;   caught 1 WARNING condition
  USE-ID

Even though safety is 0, the compiler warned us about a compile-time type problem.

[juki]

> Consider an identity function declared to only accept fixnums and returns fixnums. If you call this function with a string a type error will be signaled if run time type checks are enabled.

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. SBCL just adds them as a debugging aid, but if you rely on type errors being signaled, you have to check them explicitly with `CHECK-TYPE` or something equivalent.

> Think of soundness as a guarantee that if the program type checks

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). Common Lisp does not give any guarantee of type safety. SBCL simply tries to be helpful and catch most real world type errors, but ultimately it is the programmer who must ensure the soundness of the program.

[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