Hacker News new | past | comments | ask | show | jobs | submit login
The Unsound Playground (2016) (livecode.ch)
15 points by tosh on April 16, 2021 | hide | past | favorite | 1 comment



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.




Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: