Type systems vs. abstract interpreters
for a given a notion of type
- a type system
- is easier to specify
- it may be quite complex to move from the rules to the type inference algorithm
- needs some way of relating it to the semantics, to show the correctness (for example subject reduction)
- an abstract interpreter
- may require an abstract domain more complex than just the type
- is directly a type inference algorithm
- is correct by construction