<p>Type systems and programming languages are sometimes described as being <em>sound</em>, or <em>unsound</em>, or sometimes just &quot;not sound&quot;. What does being sound actually imply about them? Is it always the same thing, or does the context matter sometimes?</p>

<types><terminology><soundness>
What does it mean for a type system or language to be "sound"?
CC BY-SA 4.0
2023-12-15T23:32:55.427Z
It might be appropriate to tie in [mathematical soundness](https://en.wikipedia.org/wiki/Soundness), which I think is related to the meaning of soundness vis. type systems.
D. Ben Knoble
CC BY-SA 4.0
2023-12-16T15:44:33.950Z
@D.BenKnoble There is enough to talk about there that it would be worth making that into its own question (if not more than one). And before you can answer the question, you need to first answer the questions "how do type systems relate to mathematical logic? And how does 'semantics' (especially operational semantics), in the sense of programming languages, relate to mathematical logic?"
David Young
CC BY-SA 4.0
2024-01-10T04:12:48.540Z
For some practical examples see https://stackoverflow.com/questions/23939168/is-c-sharp-type-system-sound-and-decidable
Eric Lippert
<p>Soundness is a property of a type system. A type system assigns a type to a program (or expression). The assignment is sound when indeed the evaluation of that program (or expression) always yields a value of that type. As extension of this, a type system is sound when all its type assignments are sound, that it, reflect the evaluation of the program (or expression).</p>
<p>The soundness of a type system is proven against a formalisation of the semantics of a language. Both the type system and the formal semantics may capture only part of the behaviour of an actual language.</p>
<ul>
<li><a href="https://papl.cs.brown.edu/2020/safety-soundness.html#%28part._type-soundness%29" rel="nofollow noreferrer">Programming and Programming Languages - Safety and Soundness</a></li>
</ul>

CC BY-SA 4.0
2023-12-15T17:19:46.917Z
2023-12-15T17:19:46.917Z
Christian Lindig
<p>A language has a <em>sound</em> type system if every well-typed program behaves as defined by the language's semantics during execution, avoiding runtime type errors. Robin Milner, who introduced this concept, famously stated that &quot;<em>well-typed programs cannot 'go wrong'</em>,&quot; meaning they don’t get &quot;stuck&quot; during execution. &quot;Getting stuck&quot; means reaching a state which is neither a final state nor a state which can take a step according to the language's semantics.</p>
<p>There are two main approaches to type soundness: syntactic and semantic.</p>
<h2>Syntactic type soundness</h2>
<p>This approach, formulated by Wright and Felleisen, is by far the most popular. It consists of two theorems, often called &quot;progress&quot; and &quot;preservation&quot;.</p>
<ul>
<li><p><em>Progress</em>: A well-typed expression is either a value or it can take a computational step according to the semantics of the language.</p>
</li>
<li><p><em>Preservation</em>: Whenever an expression takes a step, its type does not change.</p>
</li>
</ul>
<h2>Semantic type soundness</h2>
<p>This is a more general approach. An expression of type <span class="math-container">$A$</span> is <em>semantically</em> type sound if it &quot;behaves like it has type <span class="math-container">$A$</span>&quot; at runtime. This approach takes into account how unsafe features might be used together with abstraction features to ultimately produce safe programs. Syntactic type soundness, on the other hand, is often too conservative in such cases.</p>
<p>See <a href="https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/" rel="nofollow noreferrer">this blogpost</a> by Dreyer et al. for more details. Additionally, Dreyer gives a talk on this topic <a href="https://www.youtube.com/watch?v=8Xyk_dGcAwk" rel="nofollow noreferrer">here</a>. See also the recent paper <a href="https://iris-project.org/pdfs/2024-jacm-logical-type-soundness.pdf" rel="nofollow noreferrer"><em>A Logical Approach to Type Soundness</em></a> by Timany et al.</p>
<p>There is more technical detail on what it means for a program to &quot;take a step&quot; according to a semantics <a href="https://langdev.stackexchange.com/a/3353/172">in the answer here</a>. These technical details, however, are not necessary to know if you only want an intuitive understanding of type soundness.</p>
<h1>Further reading</h1>
<h2>Blogposts</h2>
<ul>
<li><a href="https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/" rel="nofollow noreferrer"><em>What Type Soundness Theorem Do You Really Want to Prove?</em></a> by Derek Dreyer et al.</li>
</ul>
<h2>Papers</h2>
<ul>
<li><p><a href="https://iris-project.org/pdfs/2024-jacm-logical-type-soundness.pdf" rel="nofollow noreferrer"><em>A Logical Approach to Type Soundness</em></a> (2024) by Timany et al.</p>
</li>
<li><p><a href="https://courses.engr.illinois.edu/cs421/sp2013/project/milner-polymorphism.pdf" rel="nofollow noreferrer"><em>A Theory of Type Polymorphism in Programming</em></a> (1978) by Robin Milner</p>
</li>
<li><p><a href="https://www.sciencedirect.com/science/article/pii/S0890540184710935" rel="nofollow noreferrer"><em>A Syntactic Approach to Type Soundness</em></a> (1994) by Wright and Felleisen</p>
</li>
</ul>
<h2>Talks</h2>
<ul>
<li><a href="https://www.youtube.com/watch?v=8Xyk_dGcAwk" rel="nofollow noreferrer"><em>Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and now you can)</em></a> by Derek Dreyer</li>
</ul>

CC BY-SA 4.0
2023-12-15T21:35:22.540Z
2024-10-05T14:07:20.443Z
2024-10-05T14:07:20.443Z
David Young
<p>Formally, <strong>if a language is sound, for all programs <span class="math-container">$P$</span>, types <code>T</code> and values <code>v</code> that can possibly exist in this language, if <span class="math-container">$P$</span> is well-typed and an expression in <span class="math-container">$P$</span> has type <code>T</code> and evaluates to <code>v</code>, <code>v</code> is an instance of <code>T</code></strong>.</p>
<p>Informally, <strong>a type system is sound if you can't create runtime type errors, i.e. you can't assign a <code>String</code> to an <code>Int</code></strong>. To clarify, you can type up a program which assigns a value of type <code>String</code> to a variable of type <code>Int</code>, but the type-checker will reject it and the compiler won't compile it. In an unsound type system, if you make this assignment convoluted enough, the type-checker will be &quot;tricked&quot; and let you compile the program; then when you run it and the unsound assignment is executed, at best you'll get an unexpected &quot;runtime type mismatch&quot; exception when you didn't make any casts, at worst the interpreter/machine will proceed unaware and you'll get undefined and/or weird behavior.</p>
<hr />
<p>Even &quot;strongly-typed&quot; programming languages like Java and Rust may be unsound in niche ways: <a href="https://counterexamples.org/title.html" rel="noreferrer">counterexamples</a>. Strong type system ≠ sound type system and weak type system ≠ unsound type system; <strong>strong means the type system has more rules and less implicit casts, sound means that the type system's rules are consistent</strong>. Here's a program which, in older versions of Java (up to 2016), throws a <code>ClassCastException</code> despite not having any casts (<a href="https://io.livecode.ch/learn/namin/unsound" rel="noreferrer">source</a>, <a href="https://langdev.stackexchange.com/a/1449/43">related stack-exchange</a>):</p>
<pre class="lang-java prettyprint-override"><code>// Counterexample by Nada Amin and Ross Tate
class Unsound {
  static class Constrain&lt;A, B extends A&gt; {}
  static class Bind&lt;A&gt; {
    &lt;B extends A&gt;
    A upcast(Constrain&lt;A,B&gt; constrain, B b) {
      return b;
    }
  }
  static &lt;T,U&gt; U coerce(T t) {
    Constrain&lt;U,? super T&gt; constrain = null;
    Bind&lt;U&gt; bind = new Bind&lt;U&gt;();
    return bind.upcast(constrain, t);
  }
  public static void main(String[] args) {
    String zero = Unsound.&lt;Integer,String&gt;coerce(0);
  }
}
</code></pre>
<p>Fortunately, this kind of code isn't going to be written by accident, so while Rust, OCaml, and Haskell may have niche soundness issues, in practice they are considered &quot;sound enough&quot; (see the <a href="https://langdev.stackexchange.com/a/1449/43">related stack-exchange post above</a> for more explanation). But common languages have straightforward soundness bugs, including C, TypeScript, and even Java; here's an example you may have accidentally triggered which still works in Java today:</p>
<pre class="lang-java prettyprint-override"><code>class Vehicle {}
class Car extends Vehicle {}
class Bus extends Vehicle {}
public class App {
  public static void main(String[] args) {
    Car[] c = { new Car() };
    Vehicle[] v = c;
    v[0] = new Bus(); // crashes with ArrayStoreException
  }
}
</code></pre>
<hr />
<p>In formal models soundness is an unambiguous equation, but in the real world there are a few nuances:</p>
<ol>
<li><p>If a language lets you <a href="https://en.wikipedia.org/wiki/Downcasting" rel="noreferrer">explicitly downcast</a> (from <code>Base</code> to <code>Subtype</code>, like in C++ and Java, <code>(Subtype)base</code>), is it still sound?</p>
</li>
<li><p>If a language implicitly downcasts, but throws a &quot;runtime type exception&quot; instead of silently ignoring, is it still sound? (Java examples above)</p>
</li>
<li><p>If a language silently ignores type errors but never produces formally undefined behavior, is it still sound? (TypeScript, because you can have a value of the wrong type but JavaScript is nearly <code>SEGFAULT</code>-proof).</p>
</li>
</ol>
<p>I think that all 3 are considered unsound, but I argue that only 2 and 3 are problems. If you really care about soundness and the only places it breaks are explicit operations, you can just not do those operations. <strong>The real issue with unsound languages is when you accidentally, unawarely cause a soundness bug</strong>; these are painful to debug for me (and I assume most programmers) who rely on the type system and expect mis-typed values to show up at compile time, or in the explicitly-unsound casts. But to be unambiguous, I'd still call languages which satisfy 2 and 3 &quot;mostly sound&quot; or &quot;sound enough&quot;.</p>

CC BY-SA 4.0
2023-12-16T00:38:39.653Z
2023-12-16T01:57:23.593Z
2023-12-16T01:57:23.593Z
tarzh
CC BY-SA 4.0
2023-12-16T00:44:12.563Z
That Java program *does not* throw a ClassCastException; it is a static error.
Michael Homer
CC BY-SA 4.0
2023-12-16T01:17:52.720Z
I don't think an explicit cast would usually be considered unsound, technically speaking (particularly a downcast). An explicit cast can be a lot like applying a function that takes an argument of one type and happens to produce a result of a different type. Though, it does depend a lot on the specific details of the type system and the semantics.
David Young
CC BY-SA 4.0
2023-12-16T01:53:19.823Z
It looks like the Java unsound example was fixed, which means I don't trust the other counterexamples weren't also fixed, so I updated to say these languages *may* be unsound.
tarzh
CC BY-SA 4.0
2023-12-17T04:11:38.913Z
@tarzh the second Java example is a well known example of Java array (co)|(contra)variance, not present in Kotlin for example
Seggan
CC BY-SA 4.0
2023-12-17T04:11:58.433Z
Does this mean that dynamically typed languages are by definition unsound?
Seggan
CC BY-SA 4.0
2023-12-17T18:11:45.980Z
@Seggan It sort of depends on how you define the "meaning" of programs in the dynamically typed language (either intuitively in English or formally). If the behavior for all type errors is part of the semantics, then it can be considered "sound". A dynamically typed language can be thought of a language with exactly one type. Sometimes they are called "uni-typed" languages (especially by Robert Harper). Also, if you *never* have type errors at runtime, then it's likely type safe! The language with only anonymous functions and function application is like this (the untyped lambda calculus).
David Young
CC BY-SA 4.0
2023-12-17T18:20:47.423Z
This would mean that such a dynamically typed language would be sound: It only has one type, so types are always preserved (the preservation theorem holds). And if all possible behaviors are specified by the semantics (either by not having any type errors like UTLC or specifying the behavior of all errors in the semantics) and you are careful to propagate the error through all of the rules of the semantics, then the progress theorem holds. Kind of a "degenerate case" of type soundness but still
David Young
# What does it mean for a type system or language to be "sound"?
Posted by: username_0 on 2023-12-14
Type systems and programming languages are sometimes described as being *sound*, or *unsound*, or sometimes just "not sound". What does being sound actually imply about them? Is it always the same thing, or does the context matter sometimes?
**Tags:** types terminology soundness
> **Comments:**
> **username_1**: It might be appropriate to tie in [mathematical soundness](https://en.wikipedia.org/wiki/Soundness), which I think is related to the meaning of soundness vis. type systems.  
> **username_2**: @D.BenKnoble There is enough to talk about there that it would be worth making that into its own question (if not more than one). And before you can answer the question, you need to first answer the questions "how do type systems relate to mathematical logic? And how does 'semantics' (especially operational semantics), in the sense of programming languages, relate to mathematical logic?"  
> **username_3**: For some practical examples see https://stackoverflow.com/questions/23939168/is-c-sharp-type-system-sound-and-decidable  
---
## 3 answers
### Answer by username_2 on 2023-12-15. Score: 10
A language has a *sound* type system if every well-typed program behaves as defined by the language's semantics during execution, avoiding runtime type errors. Robin Milner, who introduced this concept, famously stated that "*well-typed programs cannot 'go wrong'*," meaning they don’t get "stuck" during execution. "Getting stuck" means reaching a state which is neither a final state nor a state which can take a step according to the language's semantics.

There are two main approaches to type soundness: syntactic and semantic.

## Syntactic type soundness

This approach, formulated by Wright and Felleisen, is by far the most popular. It consists of two theorems, often called "progress" and "preservation".

* *Progress*: A well-typed expression is either a value or it can take a computational step according to the semantics of the language.
* *Preservation*: Whenever an expression takes a step, its type does not change.

## Semantic type soundness

This is a more general approach. An expression of type $A$ is *semantically* type sound if it "behaves like it has type $A$" at runtime. This approach takes into account how unsafe features might be used together with abstraction features to ultimately produce safe programs. Syntactic type soundness, on the other hand, is often too conservative in such cases.

See [this blogpost](https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/) by Dreyer et al. for more details. Additionally, Dreyer gives a talk on this topic [here](https://www.youtube.com/watch?v=8Xyk_dGcAwk). See also the recent paper [*A Logical Approach to Type Soundness*](https://iris-project.org/pdfs/2024-jacm-logical-type-soundness.pdf) by Timany et al.

There is more technical detail on what it means for a program to "take a step" according to a semantics [in the answer here](https://langdev.stackexchange.com/a/3353/172). These technical details, however, are not necessary to know if you only want an intuitive understanding of type soundness.

# Further reading

## Blogposts

* [*What Type Soundness Theorem Do You Really Want to Prove?*](https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/) by Derek Dreyer et al.

## Papers

* [*A Logical Approach to Type Soundness*](https://iris-project.org/pdfs/2024-jacm-logical-type-soundness.pdf) (2024) by Timany et al.
* [*A Theory of Type Polymorphism in Programming*](https://courses.engr.illinois.edu/cs421/sp2013/project/milner-polymorphism.pdf) (1978) by Robin Milner
* [*A Syntactic Approach to Type Soundness*](https://www.sciencedirect.com/science/article/pii/S0890540184710935) (1994) by Wright and Felleisen

## Talks

* [*Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and now you can)*](https://www.youtube.com/watch?v=8Xyk_dGcAwk) by Derek Dreyer
---
### Answer by username_5 on 2023-12-16. Score: 6
Formally, if a language is sound, for all programs $P$, types T and values v that can possibly exist in this language, if $P$ is well-typed and an expression in $P$ has type T and evaluates to v, v is an instance of T.
Informally, a type system is sound if you can't create runtime type errors, i.e. you can't assign a String to an Int. To clarify, you can type up a program which assigns a value of type String to a variable of type Int, but the type-checker will reject it and the compiler won't compile it. In an unsound type system, if you make this assignment convoluted enough, the type-checker will be "tricked" and let you compile the program; then when you run it and the unsound assignment is executed, at best you'll get an unexpected "runtime type mismatch" exception when you didn't make any casts, at worst the interpreter/machine will proceed unaware and you'll get undefined and/or weird behavior.

Even "strongly-typed" programming languages like Java and Rust may be unsound in niche ways: counterexamples. Strong type system ≠ sound type system and weak type system ≠ unsound type system; strong means the type system has more rules and less implicit casts, sound means that the type system's rules are consistent. Here's a program which, in older versions of Java (up to 2016), throws a ClassCastException despite not having any casts (source, related stack-exchange):
// Counterexample by Nada Amin and Ross Tate
class Unsound {
  static class Constrain {}
  static class Bind {
    
    A upcast(Constrain constrain, B b) {
      return b;
    }
  }
  static  U coerce(T t) {
    Constrain constrain = null;
    Bind bind = new Bind();
    return bind.upcast(constrain, t);
  }
  public static void main(String[] args) {
    String zero = Unsound.coerce(0);
  }
}

Fortunately, this kind of code isn't going to be written by accident, so while Rust, OCaml, and Haskell may have niche soundness issues, in practice they are considered "sound enough" (see the related stack-exchange post above for more explanation). But common languages have straightforward soundness bugs, including C, TypeScript, and even Java; here's an example you may have accidentally triggered which still works in Java today:
class Vehicle {}
class Car extends Vehicle {}
class Bus extends Vehicle {}
public class App {
  public static void main(String[] args) {
    Car[] c = { new Car() };
    Vehicle[] v = c;
    v[0] = new Bus(); // crashes with ArrayStoreException
  }
}


In formal models soundness is an unambiguous equation, but in the real world there are a few nuances:

If a language lets you explicitly downcast (from Base to Subtype, like in C++ and Java, (Subtype)base), is it still sound?

If a language implicitly downcasts, but throws a "runtime type exception" instead of silently ignoring, is it still sound? (Java examples above)

If a language silently ignores type errors but never produces formally undefined behavior, is it still sound? (TypeScript, because you can have a value of the wrong type but JavaScript is nearly SEGFAULT-proof).


I think that all 3 are considered unsound, but I argue that only 2 and 3 are problems. If you really care about soundness and the only places it breaks are explicit operations, you can just not do those operations. The real issue with unsound languages is when you accidentally, unawarely cause a soundness bug; these are painful to debug for me (and I assume most programmers) who rely on the type system and expect mis-typed values to show up at compile time, or in the explicitly-unsound casts. But to be unambiguous, I'd still call languages which satisfy 2 and 3 "mostly sound" or "sound enough".
> **Comments:**
> **username_0** (2023-12-16): That Java program *does not* throw a ClassCastException; it is a static error.  
> **username_2** (2023-12-16): I don't think an explicit cast would usually be considered unsound, technically speaking (particularly a downcast). An explicit cast can be a lot like applying a function that takes an argument of one type and happens to produce a result of a different type. Though, it does depend a lot on the specific details of the type system and the semantics.  
> **username_5** (2023-12-16): It looks like the Java unsound example was fixed, which means I don't trust the other counterexamples weren't also fixed, so I updated to say these languages *may* be unsound.  
> **username_6** (2023-12-17): @tarzh the second Java example is a well known example of Java array (co)|(contra)variance, not present in Kotlin for example  
> **username_6** (2023-12-17): Does this mean that dynamically typed languages are by definition unsound?  
> **username_2** (2023-12-17): @Seggan It sort of depends on how you define the "meaning" of programs in the dynamically typed language (either intuitively in English or formally). If the behavior for all type errors is part of the semantics, then it can be considered "sound". A dynamically typed language can be thought of a language with exactly one type. Sometimes they are called "uni-typed" languages (especially by Robert Harper). Also, if you *never* have type errors at runtime, then it's likely type safe! The language with only anonymous functions and function application is like this (the untyped lambda calculus).  
> **username_2** (2023-12-17): This would mean that such a dynamically typed language would be sound: It only has one type, so types are always preserved (the preservation theorem holds). And if all possible behaviors are specified by the semantics (either by not having any type errors like UTLC or specifying the behavior of all errors in the semantics) and you are careful to propagate the error through all of the rules of the semantics, then the progress theorem holds. Kind of a "degenerate case" of type soundness but still  
---
### Answer by username_4 on 2023-12-15. Score: 1
Soundness is a property of a type system. A type system assigns a type to a program (or expression). The assignment is sound when indeed the evaluation of that program (or expression) always yields a value of that type. As extension of this, a type system is sound when all its type assignments are sound, that it, reflect the evaluation of the program (or expression).

The soundness of a type system is proven against a formalisation of the semantics of a language. Both the type system and the formal semantics may capture only part of the behaviour of an actual language.

* [Programming and Programming Languages - Safety and Soundness](https://papl.cs.brown.edu/2020/safety-soundness.html#%28part._type-soundness%29)
---
