3 ms·
There’s a difference between a type system and a type system that is sound. > according to the article, a type system only deserves that name if it prevents us
by avgcorrection 3y ago
There’s a difference between a type system and a type system that is sound.
> according to the article, a type system only deserves that name if it prevents use-after-free errors, memory corruption etc. etc.
Soundness is a technical term.
Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior. Imagine if a logician said the following:
- Here is my sound and complete logic
- By the way, some valid formulas will give you Undefined Behavior and I don’t care what happens in those cases
That would be pretty wild.
- DaiPlusPlus 3y ago> Things can get pretty weird if you allow memory corruption. Some languages say that certain things are Undefined Behavior UB in C allows for a lot more than just memory corruption though (c.f.: nasal demons). Also, what about alternatives to UB, such as requiring a compiler error and/or runtime fatal error?
- stonemetal12 3y agoIf we consider a program a state machine, then a sound type system is one that rules out all operations for which the next state is undefined. So Null pointer dereference is sound in Java. The next state is well defined even if it is just throw a NPE. In C it is not, because there is no well defined next state.