I'm jumping around between articles about ETCS to Simple TT to Calculus of Constructions wondering what my app should focus on.
I'm wondering, why there isn't yet a software app in which you can encode (using a mathematical language) any formal system that is given as a finite set of logical rules.
Thus Coq / Lean had to say "our software is based upon / makes use of Calculus of Constructions" in their documentation. But I'm looking for an app that can simply encode any and all of the formal systems.
I know, you're saying well that would be the programming language you choose. E.g. C++ fits the bill because it's a Turing complete language. However, this type of software won't count to answer this question. A programming language is overkill. I'm looking for a UX with an almost zero learning time for mathematicians. Learning C++ would take months.
Reason for asking.
Say I had a visual language which supports parenting of nodes, arrows between any two nodes (all arrows are parentless), and any number of text labels on a node or an arrow.
Suppose that I had a general subgraph isomorphism-based searcher (implemented in say C++ for speed) that would search for every subgraph in the drawn diagram of a user in a large graph (the database or "library") and try to match that user's subgraph to the input of a diagram rule (drawn by another user using the same language). Diagram rules get special arrows - they are two-lined arrows such as $\implies$ because they mean essentially logical implication. But we could also just label them with a keyword phrase such as "diagram rule". Anyway, if a match is made, the whole rule shows up in the library search widget allowing the user to click the "Apply rule" button which would glue in the result of the rule (and delete any nodes / arrows as needed) in place into the users graph, and create a proof step. So going one step back in the proof would show their original diagram. But the current view now shows the diagram with the logical rule applied. That rule can be part of an axiom, definition, or theorem. For example a theorem might have many associated rules so I say "part of".
Anyway, given that, clearly you can express any logical theory doing things like $x:X$ is synonymous with a node labeled $X$ with a child node labeled $x$. And an arrow can be a map of types or a diagram rule.
Okay, given that base system that is hard-coded. The theories that it has the ability to encode are any given one. The fact that we needed a graph search is only because the language is visual, and not textual, and so naturally supports commutative diagrams & graphs. Converting the language to text before doing a search seems like more work than just doing a subgraph isomorphism search.