Skip to main content

Questions tagged [soundness]

Use this tag for questions about ensuring that type systems, type checkers, or formal models of a language are sound. Soundness is a formal property about ensuring that a system only permits valid statements under its rules.

Filter by
Sorted by
Tagged with
10 votes
3 answers
823 views

What does it mean for a type system or language to be "sound"?

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 ...
Michael Homer's user avatar
  • 13k
11 votes
3 answers
307 views

How can a language statically ensure a required index exists in a list?

Suppose a language has a conventional list data structure that contains some dynamic number of values indexed sequentially. Some operations to access a value from the list require that a certain index ...
Michael Homer's user avatar
  • 13k
10 votes
1 answer
206 views

How can optional properties be made sound in a static structural type system?

Typescript's structural type system is known to be (intentionally) unsound, in the sense that the value of an expression at runtime is not always necessarily assignable to its type determined at ...
kaya3's user avatar
  • 19.7k
10 votes
3 answers
739 views

What are the consequences of an unsound type system?

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 ...
Bruce Adams's user avatar
  • 2,843