10
$\begingroup$

I was reminded in this answer (to my perhaps naive question https://proofassistants.stackexchange.com/questions/2225/what-is-needed-to-move-from-design-by-contract-to-using-a-proof-assistant) that the C++ type system is unsound.

I take this to mean that you can in theory do evil things(tm) like:

  • reinterpret_cast a string to a int or visa versa.
  • rely on undefined behaviour
  • accidentally use memory before it is allocated or after it is freed

But I also believe you can restrict yourself to a using sound subset of an unsound language. In fact formal verification is one means to achieve that. The escape hatches are there if you really need them.

So in terms of programming language design:

  • What are its benefits and limitations?
  • Likewise what are the benefits and consequences of being unsound?

You might also consider in your answers:

  • What is a good definition of soundness from the PL perspective?
  • Isn't it always possible to restrict yourself to a sound subset in a language that supports some unsound escape hatches? Like rust's unsafe keyword for example.
$\endgroup$
3
  • $\begingroup$ This Swift forums post covers soundness vs completeness pretty well, imo $\endgroup$
    – Bbrk24
    Commented Jun 8, 2023 at 19:11
  • 1
    $\begingroup$ This question feels extremely broad to me; just "what is soundness" alone would be a whole question on its own. Just the title question probably sustains itself too. Maybe it can be reasonably pared down to just a single topic (and the others into their own questions)? $\endgroup$
    – Michael Homer
    Commented Jun 8, 2023 at 21:50
  • $\begingroup$ The question is essential a "pros and cons" of soundness vs unsoundness. That obviously requires a definition of soundness. I've linked to the wikipedia one but that is more mathematical. So I'm just leaving a hint to the answerer that they might want to explain it in a more PL fashion. Still I've reword to try and fix this. $\endgroup$ Commented Jun 9, 2023 at 7:33

3 Answers 3

11
$\begingroup$

Java accidentally had an unsound type system for a decade, and nobody noticed or cared (except, eventually, Nada Amin). It had no consequences and no impact on anything in that time.

This is an extreme case in some respects, but it highlights that soundness, in and of itself, isn't always a meaningful quality in a real-world system. It's an absolute property: either you have it, or you don't. The situations that made Java unsound just never arose in real-world situations where they mattered. Here's an unsound program (from Amin & Tate, OOPSLA 2016):

class Unsound {
  static class Constrain<A, B extends A> {}
  static class Bind<A> {
    <B extends A>
    A upcast(Constrain<A,B> constrain, B b) {
      return b;
    }
  }
  static <T,U> U coerce(T t) {
    Constrain<U,? super T> constrain = null;
    Bind<U> bind = new Bind<U>();
    return bind.upcast(constrain, t);
  }
  public static void main(String[] args) {
    String zero = Unsound.<Integer,String>coerce(0);
  }
}

This was consistent with the Java Language Specification and so should have compiled, but it would crash at run time in a place where it shouldn't be able to. It's a great find and Amin & Tate did an excellent job of illustrating how it came to be. Until then, though, this problem hadn't created any practical problems. The unsoundness was lurking, but in a place that it wasn't going to do any harm. Did it matter that Java was unsound? Probably yes, still, but actual consequences are hard to pinpoint.


So what are the consequences of an unsound type system? Maybe none at all! It can also lead to serious problems at run time where data is reinterpreted dangerously. Which situation you're in depends on the language, on where the unsoundness lies, and on how people actually write code in it. Unsoundness is a necessary, but not sufficient, property to have the adverse consequences associated with it.

Languages with intentionally unsound type systems are making trade-offs for better expressivity, for performance, or for compatibility, and these consequences are generally explicitly known. Languages that intend to be sound, like Java, can be accidentally unsound, and in doing so they may still have minimal consequences; they can also open up major correctness, security, and reliability problems when properties the programmer expected to hold didn't.

If the language really is sound, it eliminates the whole class of potential errors where something isn't the type you expect it to be. That is a powerful property that you gain by giving up on some of the expressive power you could have had — and that lost power may not matter when you planned for it! Of course, it is always possible to stick to a sound subset within an unsound language, since at the very least the empty subset is sound, but in general you may lose out on a lot of the expressivity the language does have by doing that, just because the unsound parts may be very significant in a language that's designed with them in mind; you may lose nothing at all, because you're writing Java and the unsound cases would never have occurred to you.

$\endgroup$
2
  • 1
    $\begingroup$ I’m surprised that Constrain<U, ? super T> declaration is legal without a U super T constraint on coerce itself. I’m also coming from the perspective of Swift, which leans so heavily towards soundness it gets in your way sometimes. $\endgroup$
    – Bbrk24
    Commented Jun 9, 2023 at 13:41
  • 2
    $\begingroup$ @Bbrk24 That program definitely shouldn't have been permitted! It just was consistent with the rules at the time. It's broken down in the paper, but in short there were ambiguities in the rules for implicit bounds on types that enabled it (among other things). Those have all been fixed now, so the current system is sound-as-far-as-we-know. $\endgroup$
    – Michael Homer
    Commented Jun 9, 2023 at 21:25
10
$\begingroup$

Here's a straightforward definition that may be practically useful for language designers:

A static type system is sound if, whenever an expression x has a static type T, the value of x at runtime is always a member of the type T.

Note that x here is a stand-in for any kind of expression, not just an expression which consists of a simple variable name.

The consequences of unsoundness depend on the nature of the language or its implementation, particularly whether or not there is runtime type information (RTTI) which can be used to check types at runtime:

  • If there is no RTTI, or RTTI exists but is not used to check types at runtime for expressions with unsound static types, then unsoundness implies memory unsafety. C++ and Rust are in this category.
  • If RTTI is used to check the types of expressions, then an unsound static type system at worst degrades to a dynamic type system; there is not necessarily any guarantee what type an expression's value will have at runtime, but values of one type won't be used as if they are values of another type. Instead, if a sub-expression's value has an unexpected type at runtime, either an error is thrown at runtime, or the operation is evaluated by dynamic dispatch depending on the runtime type. Java and Typescript are in this category.

Memory unsafety is something that almost all modern languages want to avoid, so most languages in the first category aim for a completely sound type system. If you do choose to have an unsound type system, you must at least give enough guidance to users so that they can use it in a safe way.

This may mean offering a subset of the language in which the type system is sound (e.g. Rust without unsafe), or writing a detailed specification for what the programmer must ensure about their own code to guarantee memory safety (e.g. the Rustonomicon). In the latter case, it's the programmer's job to prove for themselves that the types of their expression are correct, and the compiler cannot check the proof.

Languages in this category only really benefit from unsoundness to the extent that there are useful, correct programs which can be written in the language but whose correctness the compiler cannot verify.


On the other hand, languages in the second category can benefit considerably from unsoundness; since memory safety is still guaranteed (the implementation checks at runtime before doing anything that might be unsafe), an unsound static type system can be thought of as somewhere along the spectrum between dynamic types and (sound) static types. This gives gradual typing.

There's a much bigger discussion to be had about the advantages and disadvantages of gradual typing, and I think it's out of scope for this question, but I'll point you at a few other Q&As which are more-or-less relevant:

$\endgroup$
1
  • $\begingroup$ One thing that annoys me is how little priority some language maintainers seem to place upon the ease of maintaining memory safety. Many programs will be fed a mixture of correct and nonsensical data, with very loose requirements on how some forms of invalid data are handled. Having a programming language provide just enough built in checks to ensure memory safety may be much cheaper and safer than requiring that programmers include much more rigorous checks to prevent all meaningless operations that could result from nonsensical data, but some language maintainers favor the latter approach. $\endgroup$
    – supercat
    Commented Nov 10, 2023 at 16:39
6
$\begingroup$

Well, there's a whole web site — Counterexamples in Type Systems — that lists all main sources of unsoundness in type systems and their consequences.

In general, in sound type systems "well-typed programs cannot go wrong" — they don't crash, don't corrupt memory, don't throw exceptions (unless intentionally), don't have data races and so on (the list varies from language to language and type system to type system). In unsound type systems you don't have such guarantees...

So if you have certain guarantees at compile-time (through sound type-checking) you don't need to check the same thing at run-time, meaning you can have both fast and safe programs. OTOH if you want safety in an unsound language, you'll have to perform these checks at run-time. There's no free lunch. Some languages just go unsafe — check neither at compile-time, nor run-time — but I wouldn't call it a "free ride"...

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .