Mathematically showing what is possible? I apologize in advance if this seems like a silly question - I have absolutely no experience in this branch of math.
So, let's define a 'programming language' that starts out with an empty string $s$ and can do the following:


*

*Receive inputs $a$ and $b$

*Loop, either a set number of times, $a$ times or $b$ times

*Append any letter to that string

*Output the number of letters in s. 


Now, it is obvious that you can add and multiply numbers in this language, but what if it wasn't? What if we had a more complex set of rules or more complex goal such that  intuition couldn't tell us whether the goal was possible or not? How could we mathematically prove that something in that language was possible or not possible?
Simply speaking, how, mathematically, given a language with a set of rules and functions, can you see if something is possible or not? 
 A: To show that something is possible, we normally just describe a program in the appropriate system to do it. 
There are at least two ways to show that something is not possible.  The first is the method of diagonalization. This is used to show the uncomputability of the halting problem, the uncomputability of the Busy Beaver function, and similarly the uncomputability of many other functions. 
The second method is by finding an external characterization of the functions in a particular system, and then showing that the function we have in mind does not meet that characterization. That shows the function we have in mind cannot be constructed in that system. This method is used, for example, to show that Goodstein's theorem is not provable in Peano Arithmetic, and therefore the associated function is not provably total in Peano Arithmetic, although it is a total computable function in the ordinary sense. 
For an example of the second technique, consider the formal system in the question. We can prove that for each particular program $P$ in that system there is a polynomial $q_P(n,m)$ so that output number $P(a,b)$ is $q_P(|a|, |b|)$. Thus the function that takes $a$ and $b$ and returns the number ${|a|}^{|b|}$ is not computable using the system in the question, because the function $n^m$ is a polynomial of $n$ and $m$. 

Proof of the characterization. The proof of the polynomial characterization is by induction on the structure of the program. It may seem surprising because the language is not much different from LOOP, and LOOP is able to compute all primitive recursive functions. But the system here is different enough. 
The basic operation of the program is to append a single letter to the output string $s$, which is to say add 1 to the length of the output string. The strings $a$ and $b$ don't change, the output string never gets shorter, and loops run either a constant number of times, $|a|$ times, or $|b|$ times. 
We need to check three programming constructs: concatenation, appending a single letter to $s$, and looping. 
If we concatenate two programs $P_1$ and $P_2$ to make a program $P$, the work done by $P_1$ will not affect $P_2$. We can ignore the fact that $s$ will not start out empty when $P_2$ runs, which also will not affect $P_2$. Thus we will have $q_{P}(n.m) = q_{P_1}(n,m) + q_{P_2}(n,m)$.
The program that appends a single letter to $s$ has polynomial $q(n,m) = 1$. 
Finally, suppose that we have a program $P$ which we wrap in a loop to make a larger program. We want to show there is a polynomial $q(n,m)$ for the new program. According to the rules for our system. each iteration of the loop will append the same number of letters to $s$; there is no way for the program to change how many letters are appended on each iteration. So we just need to multiply by the number of iterations.  If the loop runs $|a|$ times, we can take $q(n,m) = n\cdot q_P(n,m)$. If the loop runs $|b|$ times, we can take $q(n,m) = m\cdot q_P(n,m)$. If the program runs a constant number of times, $c$, we can take $q(n,m)  = c \cdot q_P(n,m)$.  
A: The branch of mathematics this seems to be in is the theory of formal languages.  In particular, you are asking about the capabilities of a formal grammar: https://en.wikipedia.org/wiki/Formal_grammar
A: So the question you are asking is very interesting and concerns some very deep areas of mathematics. 
Let us break it down: 
"Simply speaking, how, mathematically, given a language with a set of rules and functions, can you see if something is possible or not?"
Let us forget if our sentences have ANY meaning, suppose I just give you a set of rules (ex: we can append letters to a string of even length, we can cut strings into thirds and keep the largest third, the letter "a" is a valid string, etc...) IS some specific string X, a valid string in the language?
This is impossible to do in the general case, and extremely extremely hard to do in some relatively simple cases. Why? 
Consider mathematics itself. Suppose I listed all the rules for modifying valid sentences in proofs in some fixed system of logic that includes arithmetic. Then this "System" is at least as complicated as arithmetic as we know it, and therefore, there is a way to take any problem in arithmetic and convert it to a problem here. 
Now suppose I had a finite length mathematical procedure that is able to verify if a statement in my new language is "generateable" or not. Then I could take statements in peano arithmetic, for example "does there exist natural numbers $x,y,z,n$ not equal to 0 or 1, wit n > 2, such that $x^n + y^n  = z^n$", and use our procedure to quickly tell, whether the given statement IS a valid theorem or isn't. Allowing us to automate the process of finding proofs to hard problems, such as the famous Fermat's Last Theorem that I gave. Revolutionary! But,
Kurt Godel showed that this is impossible to do in the general case. Not as a limitation of human capability or creativity in building algorithms. It just CANNOT be done in general for the same reasons that "1+1=2", blowing a crushing swing to one of the largest unsolved problems posed at the time by Hilbert (who also was hoping we could SOLVE all of mathematics). 
Now the actual proof that Godel uses is a bit complicated (perhaps worth a google) but it can be explained very simply in a different way that later we realized was the same paradigm (courtesy of Alan Turing):
There is no finite length program C, that given another computer program X as a string, can decide in finite time if $X$ halts or doesn't for any reasonable model of computation. 
Known as the Halting Problem, this has a very elegant although, at first mind bending proof by contradiction. Suppose we had the program $C$ in front of us, that can solve this problem. Then we can consider the following program:
(Things preceded by a # aren't part of the code, just comments to explain what the code is doing)
Filename: P.txt
import C #the program for solving the halting problem
open("P.txt") #the program grabs its OWN source code
if C decides P.txt halts:
    While(True): #if C decides P halts, then P is programmed to run forever

if C decides P.txt doesn't halt:
    return 0  #if C decides P doesn't run forever, then P stops.
End Program

So by definition $C$ cannot correctly determine if this program halts. Namely if $C$ actually exists in real life, if a program that can always solve the halting problem, on all finite length programs, exists, then this same C cannot SOLVE the halting problem on this finite length program P. Summarized:
If C exists then it doesn't. 
So we conclude, C cannot exist in the first place, and thus this problem cannot be solved.
Why did I bring this up? Because going back to "Systems of Mathematics" we can create a system where the theorems aren't of the usual form "There exists infinitely many prime numbers etc...", but instead the theorems are just "This program (program description here) does/doesn't halt". And this can then be reduced, to another symbol system, using the same procedure I described above. And now the problem of "recognizing" if a system of math can produce some sequence of characters, is equivalent to asking if there is a procedure to solve the halting problem, which we now know rigorously as impossible
But what if the system of math we are dealing with, isn't THAT powerful. Maybe we have a relatively simple system of producing sentences. Even then the question rapidly becomes challenging and is filled with interesting work. See the MU Puzzle of Douglas Hofstadter, (I highly recommend if you like this stuff to check out the book Godel Escher Bach by him, it features a lot of tasty tidbits along this line of thought, and yet is written in a way that the average layperson can thoroughly enjoy. It won a pulitzer prize in fact!). 
But to summarize, yes for suitably simple systems we can indeed generate such algorithms, BUT, the complexity of these algorithms and ideas they require can quickly transcend what the system itself is capable of doing, and so even if you know this problem is solvable, it is very hard and very fun to try to work on it. 
