What is a sound programming language?

Question

According to Dart's website

Dart is a sound language.

What's the meaning of "sound" in the above sentence?

I couldn't find any similar concept in other major programming languages. Can anyone give some other examples of sound languages?

Answer 1

Taken from Dart's language guide

What is soundness?

Soundness is about ensuring your program can’t get into certain invalid states. A sound type system means you can never get into a state where an expression evaluates to a value that doesn’t match the expression’s static type. For example, if an expression’s static type is String, at runtime you are guaranteed to only get a string when you evaluate it.

Strong mode, like the type systems in Java and C#, is sound. It enforces that soundness using a combination of static checking (compile errors) and runtime checks. For example, assigning a String to int is a compile error. Casting an Object to a string using as String will fail with a runtime error if the object isn’t a string.

Dart was created as an optionally typed language and is not sound. For example, it is valid to create a list in Dart that contains integers, strings, and streams. Your program will not fail to compile or run just because the list contains mixed types, even if the list is specified as a list of float but contains every type except floating point values.

In classic Dart, the problem occurs at runtime—fetching a Stream from a list but getting another type results in a runtime exception and the app crashes. For example, the following code assigns a list of type dynamic (which contains strings) to a list of type int. Iterating through the list and subtracting 10 from each item causes a runtime exception because the minus operator isn’t defined for strings.

The benefits of soundness A sound type system has several benefits:

Revealing type-related bugs at compile time. A sound type system forces code to be unambiguous about its types, so type-related bugs that might be tricky to find at runtime are revealed at compile time.

More readable code. Code is easier to read because you can rely on a value actually having the specified type. In sound Dart, types can’t lie.

More maintainable code. With a sound type system, when you change one piece of code, the type system can warn you about the other pieces of code that just broke.

Better ahead of time (AOT) compilation. While AOT compilation is possible without strong types, the generated code is much less efficient.

Cleaner JavaScript. For web apps, strong mode’s more restrictive typing allows dartdevc to generate cleaner, more compact JavaScript.

---

Bringing soundness to Dart required adding only a few rules to the Dart language. With strong mode enabled, the Dart analyzer enforces three additional rules:

Use proper return types when overriding methods.

Use proper parameter types when overriding methods.

Don’t use a dynamic list as a typed list.

Answer 2

That is NOT related to audio.

According to Wikipedia:

That is, if a type system is both sound (meaning that it rejects all incorrect programs) and decidable (meaning that it is possible to write an algorithm that determines whether a program is well-typed)

(cf. https://en.wikipedia.org/wiki/Type_system#Static_type_checking)

For consideration about etymology, see "soundness".

TL;DR: in this context, it means "robust", "healthy".