Counterexamples in Type Systems
The website "Counterexamples in Type Systems" collects examples of programming language type systems that are unsound, meaning they accept programs that crash or violate type safety at runtime.
Background
A growing, community-driven catalog of programming-language edge cases — snippets of code that compile (or are accepted by a type checker) but then crash, contradicting the language's own safety promises. Each entry names the language, shows the surprising behavior, and explains why it violates an expected invariant. Useful for PL theorists, language implementers, and working developers who want to know where a language's type system bends or breaks. Hosted by (and in part written by) Matt Might, a well-known PL researcher and former professor at University of Utah.