> This stuff often ends up explained in very academic language,
What, that software should be correct according to the specification (either a formal one or an informal and implicit one)? Because that's the academic motivation I've found for things like type systems and program specification.
I mean like "Curry-Howard isomorphism" and "state space" and "monad" and such. It makes it very easy to dismiss as academic wankery, which is helped by the fact that, well, yeah, some of it is, honestly. But under that academic wankery is some brilliantly practical stuff that is hard to learn from the communities that are over-focused on "practicality".
What, that software should be correct according to the specification (either a formal one or an informal and implicit one)? Because that's the academic motivation I've found for things like type systems and program specification.