I've been really getting (topically, hence the question) into formal logic and formal languages lately. I find the topic quite interesting. A lot of papers and posts that I read about formal languages are interesting (and a good amount are of computational nature), but overall revolve around the same subject -- languages, of course. My question is how are these things useful? For computational purposes, I see how the expressive power of, say, in particular, Domain Specific Languages is a good way to go about things, but this doesn't seem to contribute to the overall state of well-being of mathematics on the whole. I mean, perhaps there's something there (beyond expressiveness), but I don't see it, and it comes off more as a gimmick, than a really demanding-and-rewarding mathematical discipline. So the question is -- and for some reason I get the impression that this is somehow a burning question in many people's stomachs -- how does research in mathematical logic, say model theory and formal languages in particular, then, contribute to other, general-purpose mathematics, beyond assuring that the foundations of mathematics are rock solid?
Topology and geometry give back to logic in HoTT, so does algebra of course, on which modern logic currently rests. Banach and Tarski do give a seemingly paradoxical construction in geometry and topology, but this seems to be more so an exercise in logic itself, than a contribution to geometry right? I mean it goes something along the lines of "well, if we buy into the axiom of choice, (or alternatively, ZF, or a bunch others if I understand correctly), then here's what's possible and "a pea can be chopped up and reassembled into the Sun" ". Similarly, if we take non-standard analysis; here, again, this is, as far as I understand, an exercise in a "better" (different, if you disagree ;) ) interpretation of analysis.
So, while I completely agree that these are fascinating mathematical exercises in their own right, that mathematical logic deserves attention for it's own merits, and that mathematical logic is demanding-and-rewarding in it's own right, I am having trouble seeing how that percolates into other areas of mathematics. I.e., can logic give NEW results in algebra, geometry/topology, analysis/probability, or even cobinatorics/graph theory?