All of the mathematics that I know are founded on set theory ,i.e., high school mathematics , calculus and real analysis , little of group theory and topology .But I have gotten to know that there are alternate foundations of mathematics (or maybe some branches of mathematics) like category theory,type theory etc . Some sources mention these foundations of mathematics as programming languages of mathematics.
Programming languages differ from each other in their internal mechanism ,i.e. , the way the compiler written for them generates machine code ,the way their compiler allocates memory and some other things like linking .The machine code generation on matching with the simplest code to accomplish a particular operation yields faster performance and similarly the memory management affects the addressing of the variables , their manipulation etc .
As such every language have their own merits and demerits in terms of speed and ease of tasks.
(please read the above paragraph without subjecting it to detailed theoretical and technical scrutiny as this is a very rough and sketchy idea )
Are there any analogous comparisons between these different programming languages of mathematics or foundations of mathematics . What can be analogous to the process of compiling or linking or what can be analogous to memory allocation ? If yes then ,Are there any such instances of proofs which are very hard to do in one foundation of mathematics but are conjured marvelously in an alternate foundation of mathematics and the differences in the difficulty of the proofs being explained in the manner of programming languages ?
Similarly , even without going to other foundations of mathematics , we can see that there are many instances where theorems are proved in many different ways . Like , infinitude of prime numbers , one having proof by contradiction by gauss and the other in the language of topology by Furstenberg (although this one is also a proof by contradiction). A better example might be Fermat's last theorem which is proved in combinatorial way , group theoretic way ,through dynamic systems . And similarly , there is a Fermat's theorem on sum of squares , which has one long proof by Euler to a one sentence proof by Zagier.
In all these instances , we can see that the same process is being accomplished in different languages , some in the languages of topology , some in the languages of group theory, some in the language of dynamic systems etc . Do we have any analogous parameters like memory management of the compiler of the language , by which we can explain why some of these proofs were easier than the other ones or like we can say some settings or languages allowed better expressions or better access to somethings which were difficult in another language .
(There's a heavy chance that this question might be flagged as unclear about what it demands . Basically , I want to know whether there have been instances where proving something turned out to be very easy in one foundation of mathematics but impossibly difficult in another .Can we do an comparison in such cases between these foundations analogous to comparing internal mechanism of programming languages to reason the difference between them in various aspects .In such cases , what parameters or factors can be analogous to factors like memory allocation ,optimized machine code ,etc.)