Whenever I see like this, I ask, "have you ever worked on a team? Have you ever worked code without anyone who originally wrote it being around?" Dynamic typin

Whenever I see like this, I ask, "have you ever worked on a team? Have you ever worked code without anyone who originally wrote it being around?" Dynamic typing only works small / solo projects and those that love to be obscure for fun. The things they want to do are...largely ill-advised. Because the problem they talk is about is less static typing, but structural vs normal (or transparent vs abstract) types. You can't "reverse an Automobile" for good reason! It is good they are aware of dependent types, but > Additionally, Idris features computational effects, elaborator reflection, coinductive data types, and many-many stuff for theorem proving. With This is attacking a strawman. Yes, Idris is a kitchen sink. But they also don't need any of those features. They could have used Agda for the example, and Agda is quite a small language! And still, I return to the stuff at the top. Reflection, breaking parametricity, etc. are all banned for good reason -- their midwit meme is off it is Zig etc. which are the midwits. Monotonicity (e.g. with traits) and parametricity are important metatheoretic properties for reasoning about code. Bottom line is this person wants to do things I would reject in code review regardless of the language.