Note: I am interpreting “algorithms” broadly, to include algorithms that require an infinite and even uncountable number of computational steps.
It seems to me that any definition can be seen as a specification of an algorithm in this sense: For example, consider the definition:
$$X=\{x:\mathbb R| \chi(x) \}$$
This specifies an algorithm: Check for each $x\in \mathbb R$ whether the property $\chi(x)$ is satisfied. If it is, add $x$ to the set $X$.
Question: Can we see all mathematical concepts as specifications of algorithms (possibly requiring uncountable computational steps)? Is there some kind of theory that formalizes this idea?
Why am I asking this? Because it seems to me that if this is true, then this suggests to me a deeper connection between math and computer science than I thought:
very eye-squinty: computer science treats the intension of concepts, and math treats the extension of concepts.
whether something is “computable” simply means whether there is a finite algorithm for it. Everything is computable in an infinite sense.
We can think of all of math in computational terms, even in uncountable contexts
Theorems about connections between different areas of math become theories stating that two different (possibly uncountable) algorithms produce the same output.
The difference between classical vs constructive logic and math, is that classical math allows for infinite/uncountable algorithms.
TL;DR: Probably yes.
A formal system is a collection of axioms and inference rules over an alphabet that can also include metavariables. Any inference rule has a finite collection of premises and a single conclusion, metavariables may be replaced by arbitrary words, since all terms are also generated by the system.
There is a system modeling the notion of formal systems itself which captures all formal systems and all statements provable within them, such that every mathematical statement provable in a given context can be proven within this system.
It is quite obvious that a program generating all valid statements in this metasystem exists, yet it would run in uncountable time, even if we assume finite alphabets and words of finite length.
This program would be able to prove as much as a system allows, undecidable problems just wouldn't be included in the eventually generated result. At the end (after an uncountable amount of time), not only all provable statements of ZFC set theory, but also all such words of type theory, second-order arithmetic, ..., any system that can be specified in this very formal way will be computed.
Since you want to treat specific problems as programs, you'd just need to fit the statements returned into a certain scheme, such as the set builder notation you used. Then, the problem can be solved for $X$.
The difference between classical and constructive logic you mentioned doesn't seem fitting in my eyes though. In intitutionistic type theory (which is definitely constructive), there are types with an uncountable number of inhabitants. They need to be treated a bit more carefully, though.