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
5 votes
1 answer
317 views

Can final and full lattice type theory be combined?

Let us assume a language that has final with Java semantics, i.e. a final type cannot have subtypes. Further, let that language have a full lattice type theory with at least one bottom type, e.g. ...
feldentm's user avatar
  • 1,779
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
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
11 votes
1 answer
438 views

How can I have mutually-exclusive properties in a structural type system?

I have a structurally-typed object-oriented language, and I'd like to allow for types with some mutually-exclusive properties/attributes/slots/methods. That is, an object having more than one of these ...
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