It's really satisfying fixing crashes in rust-analyzer. You can start from a panic message and dig until you've got a tiny Rust program that triggers the problem.
(It's usually an issue with incomplete source files breaking invariants.)
Untyped programs don't exist: https://www.williamjbowman.com/blog/2018/01/19/untyped-programs-don-t-exist/
Demonstrates a simple theorem, but has a nuanced notion of types as invariants. It discusses the important questions of when we should check types, allowing escape hatches, and whether type checking should be decidable.