The Unsound Playground (2016)

A very cool and surprising result that I always thought should've received more fanfare in non-PL circles.

Just as a little extra context on what "unsound" means here since the term is often misused or used in different contexts: this program violates "type soundness", which is informally stated as "well-typed programs don't go wrong".

Generally you'll see this shown via a "progress" lemma (~ "all non-value expressions can take a step in the operational semantics") and a "preservation" lemma (~ "expressions' types are unchanged by the operational semantics") which, by induction, yield a theorem like "all expressions of type T can be evaluated to a value of type T" (for all T).

This paper, since it deals with actual programming languages and not minimal calculi, may feel a little bit removed from the theoretical stuff, but under the hood it's the same idea: preservation doesn't hold when applying `coerce`, so well-typed programs _can_ go wrong.

There's some great discussion in Section 6.3 about the (abundant!) literature on Java subsets/core calculi, and both the benefits and limitations of using such languages to reason formally about actual PLs.