Counterexamples in Type Systems: programs that crash, segfault or explode (2021)

Fun fact: even theorem provers have counterexamples - Breaking Badfny: https://www.reddit.com/r/Coq/comments/x4d31y/breaking_badfny... - Falso (Coq): https://github.com/clarus/falso - Coq critical bugs (some of these mention potential ways to prove false): https://github.com/coq/coq/blob/master/dev/doc/critical-bugs (You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times!)

I study type systems and programming language theory at university, and I encourage friends studying CS to at least have some understanding of type theory, such as well-known type systems (simply-typed, System F) and properties like soundness or uniqueness of typing. Why? Because as programmers we argue to death comparing the expressiveness and properties of type systems of our favorite programming languages, or we're picking up a language with features like traits or type inference. Type theory really lets you…