Yes, you could say that the C standard is a formal theory. It won't be a very interesting one to a mathematician though, because it's huge and describes only one thing, C. There are no special considerations to single out that theory from a huge pool of similar ones. It's like devoting your life to the study of one particular differential equation with a thousand terms, which was written by a committee. Why not the other equation which has a minus instead of a plus over there? Why not study differential equations in general?

Compare with a formal theory like PA, which fits on a page and describes the natural numbers. Proving a theorem about PA has implications everywhere, because natural numbers are everywhere. Or if we want to talk about computation, there are many formal theories with short descriptions that have much more to say about computation in general.

I am not against your POV ! I think we largely agree on most things here. I wanted to correct what I perceived to be a mischaracterization of my 'off the cuff' analogy.

Yeah, from your reply to patrickmclaren I understood the point you were trying to make, and I agree with you. Sorry for misunderstanding you so persistently.

Can you deduce the majority of the C language from these initial axioms?

You misunderstand the usage of consistency regarding mathematics. It is not the same. These rules which compose C are design decisions, and whether they are entirely artificial. Mathematical consistency arises from imposing axioms, following which there are no decisions to be made.

>Can you deduce the majority of the C language from these initial axioms?

Well, no. You can deduce A language but it might not be C.

I sense we're going down a fruitless path here. In my first post I was only giving an analogy of someone understanding math at a fundamental level to someone understanding a programming language at a fundamental level and how they could inform similar abilities/prowess in people when it comes to dealing with complex problems/etc.