I have a question, and maybe it is already something that exists. But I do not know and hence asking here (also kind of food for thought). I was wondering if there is any language which has been designed from ground up to make mathematical formalism as a first class citizen. Precisely I was thinking some kind of way to write set builder notation and then built-in functions to perform and generate (here the generate word is used in a double meaning, think about generators, as some of those operations can generate infinite data) basic operations, such that intersection, union, sigma algebra, and such? It is something I am thinking. As having something like this will open up doors to programming into a lot of mathematical domains pretty accessible. Topology, Measure theory, Order Theory, Category Theory etc. etc.

Consider Agda, for example this recursive set tutorial: https://people.inf.elte.hu/divip/AgdaTutorial/Sets.Recursive.html#1

Not sure anything corresponds exactly to what you are looking for, but Lean (https://leanprover.github.io/about/) is certainly worth a look, as are other proof-oriented languages such as Coq's (https://coq.inria.fr/) underlying language Gallina. Computer algebra systems are another candidate. Axiom (https://github.com/daly/axiom) is huge but also the most likely to contain what you are looking for. There are also more specialized systems popular in specific branches of mathematics, which unfortunately I don't know much about.

Thanks both of you. I will look into them. Also, interesting to see what it (may) take to build such a system with an extension / library system built in so that people can take the basic system as extend it to the domain they are interested into

Fortran was designed to do exactly that

I mentioned this in a other thread but Pure Lang has many pieces that make it useful for both symbolic and computational mathematics

Do you have in mind examples how such a language would be used and what it would be used for? What kind of programming would you do with topology? If it is theorem proving in topology then lean seems like the kind of language you're looking for. Just curious.

I do not have any example right now. It was more of a curious question. However, I am interested in probabilistic logic programming (https://github.com/ML-KULeuven/problog). And machine learning. I have a strong feeling that we can use them together (https://bitbucket.org/problog/deepproblog/src/master/) however, I was wondering that whether we can extend the symbolic domain significantly. And from that thought, this one followed. '

Yeah, I've a big old directory of probabilistic programming resources, which I plan to ignore hoping for more coherent theory and practice to emerge before I get around to reading any. 😉

You might like: http://pll.cpsc.ucalgary.ca/charity1/www/examples.html as it is based on CT.