Exhaustiveness checking in Rust, Java, PHPStan

This post is all about modeling the potential paths a program can take, via the programming language’s type system. First I give a quick introduction about the core ideas, with examples written in PHP. Then, I show how Rust and Java expand on these ideas. And in the end I circle back to PHP (with a static analyzer), trying to model the program in a similarly advanced fashion. I think the possibilities and limitations are quite fascinating. My goal is not to say „language A good, language B bad“, but to show their state of the art. I learned a lot while working on this article and hopefully you too will find it interesting!