My understanding is that a programming language designed for “doing math” would basically:
- Be able to represent mathematical ideas (hopefully in a similar way to non-programmatic mathematical notation)
- Have some kind of transformation rules relating changes in the form of an expression to ideas of valid “logical inference”
To me this makes me imagine such a language could be used for meta-programming, like, for any expression, I can apply some rule / function to transform the function into a new, valid form.
I suppose that in the same way, it can act as a proof-checker, maybe if parsing a series of expressions or “executing” it just results output of whether or not it was “executable”.
I guess I am curious to know about how this works, what goes on under the hood?
I’ve read around and it seems like people talk about how each language like Agda or Coq or Lean has its own particularities, assumptions it has made about what type theory or kind of set theory it is based on, what axioms it assumes.
But ideally, is there any type system, in view of modern mathematical attempts to view all such systems abstractly, which underlies all such choices? Like a most flexible or foundational proof assistant language / type theory?
Which type theory is that?
And, is there a programming language which uses it? If not, why not?