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.
6
questions
5
votes
1
answer
326
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. ...
- 1,969
10
votes
3
answers
873
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 ...
- 13.1k
11
votes
3
answers
316
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 ...
- 13.1k
10
votes
3
answers
800
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 ...
- 2,853
11
votes
1
answer
444
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 ...
- 13.1k
10
votes
1
answer
207
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 ...
- 20k