Superb article on type systems, open vs closed world soundness, and type systems intentionally not offering soundness: https://frenchy64.github.io/2018/04/07/unsoundness-in-untyped-types.html