Re:Parse, Don't Validate (2019)
by justinpombrio on Saturday June 26, 2021 @02:21PM
(#27644442)
A type system is sound when:
Notice anything interesting about this definition? It uses the word "evaluate"! Type soundness is not just a statement about the type checker. It relates type checking to run time (and thus to compilation too). That is, if you muck with Java's runtime or compiler, you can break type soundness, even if you don't change its type system in the slightest.
[ Parent
| on HN ]
Yes this is precisely what I am talking about.
Different implementations of eval() a.k.a different programming languages have different semantics.
Which implicit eval() implementation does the above hold?
What type system do you have in mind such that the above holds for ALL expressions. Type-checking itself is not always decidable.