I originally wrote a draft of this in December, but was inspired to finish it by recent events (i.e. actix-web). We’ve all heard the trope that the “free” in “free software”
Position: Type annotations are ultimately undesirable when working with sufficiently-complex type systems, but there is no better solution. There is a point where a formally-verified compiler becomes indistinguishable from an automated theorem prover.
From the bottom of my heart, I really and truly hope that somehow I am proven wrong... but we all know that's not going to happen.
The figures we mock the most might just be the ones who represent us best.