Whether you're right or not depends on whether one believes that algebraic datatypes could only have come out of a fascination with the "mathematical properties

Whether you're right or not depends on whether one believes that algebraic datatypes could only have come out of a fascination with the "mathematical properties of the type system". Because ADTs are a serious win in terms of robustness and efficiency of development. They are now found in Rust (for example) but were invented in the 70s in the functional language community. An innovation like that, which was not stumbled on by mainstream imperative language designers, arguably comes from a focus on abstract mathematical structure. You might be right if you believe that profunctor optics are going nowhere, or that dependent types and type–level programming are just too complicated, but as a research project, strongly typed functional programming has many strengths, and I don't just mean strengths that are not essentially related to the type system like purity or laziness. '“The ability of the [strong] type system to catch [mundane] errors allows us to spend more time thinking about other, deeper issues in our code and drives down our error rate, making it possible to move faster while still maintaining safe and reliable systems,” says Yaron Minsky, co-head of the technology group at liquidity provider Jane Street. The firm, as it puts it, writes “everything that we can in OCaml”, a functional language, and employs 300 OCaml developers.'