What's not mentioned in the comment you're replying to is the postgraduate-level type theory you need to learn and constantly refine to work with these languages at a practical level. So be aware that even if you put the time into learning them, it's unlikely you'll get to use them at work.
Look up Coq, Agda, Lean, and Idris. I would start with Coq, it's the most used. Idris is more like Haskell and programmer-oriented.
Edit: Nevermind, apparently they were just talking about Haskell...
I'm more thinking in terms of logical primitives for the design of modules and components that can be composed, decomposed and recombined. I'm thinking less about proof based correctness.
On some level, all of them do. Programming lives in a grey area between human language and discrete, symbolic logic.
The way in which we get to an "application" is in designing interfaces that look more like the domain, and less like the implementation. If you can define the math you're using symbolically, you can apply it directly to express ideas from, e.g. linear algebra, set theory, graph theory. And libraries exist for all of those things - you can make the interface more convenient with additional syntax and compiler assistance, and you can frame the program in terms of theorem-proving logic(which is the realm of stuff like Coq) which provides an extra degree of assurance that the program does the thing you defined it to do by adding more detail to that definition, but often the problem requirements fit in the realm of "just tell the computer to do things" - and so imperative code is the default, everywhere.
But we can also take concepts like "name", "job", "age", "ethnicity", "gender", and enter them into a computer. And all of those are human ideas, socially constructed and philosophical in some degree. Mathematics doesn't help us express the essence of those ideas, it just tells us of ways to symbolize the tokens involved, which can be made relatively general and flexible but all of which ultimately stem from a predesigned enumeration of options like the codepoints available in UTF-8 or the range of values in a 32-bit integer.
And a lot of the mathematical stuff is subsumed by the social/philosophical in practical application: we agree that the data has some kind of truth to inform us, because it's compatible with our framework for understanding it. And if you have a setup that fits the model of computing, something like taking a sensor that emits numeric values at a regular frequency and processing the output into some kind of signal - then you can program mathematically all throughout. But if you're mostly dealing with human language, you're constantly hammered with interface problems for other reasons.
Human concepts can be placed under mathematical interfaces.
Inversion for gender
~male = female
Ordinality for human hierarchies:
CEO > manager > worker
Commutativity for human action:
Punch human + kick human = damaged human
Kick human + punch human = damaged human
Mathematical interfaces are different from mathematical primitives which I believe you have mistakenly combined into a singular concept in your response.
By fitting human concepts into mathematical interfaces you develop a sort of algebra dsl for the language allowing you to apply all mathematical theorems of the equivalent algebra to the domain. Those theorems are the generalities that improve design by improving modularity.
Suddenly for ordinal concepts I can use a general min or max function across all domains. By using mathematical interfaces I am in the realm of the ultimate generality. Normally people would be writing some form of equivalent logic to derive the lowest ranking human in a hierarchy when really the concept of min covers it.
These basic mathematical interfaces that apply to basic numerical logic are found to be expandable across domains. There's no proof or logic as to why these interfaces happen to be more universal. It's just a gut feeling after using this interfaces more that they happen to be extremely universal. Thus there's no way I can prove to you what I'm saying is correct, you ultimately have to try it.
The language of math itself is functional. In fact "functional programming" is basically programming as if everything was math. Think about it, does math allow for variable mutation inside a mathematical expression? No.
Interfaces that mutate internal values do not exist in mathematics. So, in essence, yes. Mathematical interfaces only support functional operations.
Is this really true? Have you written idiomatic Haskell before? Not trying to question your familiarity if so, but a large part of doing so is utilizing interfaces that do just that.
One of the most critical parts necessary to fully grok idiomatic Haskell is how it uses mathematical interfaces, specifically category theoretic interfaces to structure internal state mutations -- specifically Monads and other structures. This specific interface utilizes two properties, identity and associativity, to do this and create one-way, sequenced computations still couched in formal rigor and laws.
Contrasted to other languages, in order to do any useful I/O in Haskell, one needs to understand and use Monads. Of course, the utility of the Monad includes but is not limited to just this use case.
