I am not very sure what you are asking, and I am also not sure that you have the background to understand CompCert. It seems that you are still confused by some basic concepts in Coq.
I would suggest you start with Software Foundations. Most of your questions would be answered there.
But, basically:
* Definition and Fixpoint are like OCaml's let and let rec, respectively. They are used to define values and functions (and, of course, propositions).
* Inductive is like type in OCaml, or datatype in SML. They are used to define algebraic data types (or "inference rules").
* Prop is the sort of propositions, so Definition and Inductive that return Props are defining propositions (i.e., "proof rules"). The Definition and Inductives are not themselves proofs.
* <PERSON>, Theorem, Corollary, etc...are used for proofs.
* Coq is based on the <PERSON>-Howard correspondence: a proof of the proposition $A \rightarrow B$ is a function that takes something of type $A$ and produces something of type $B$, a proof by induction corresponds to a recursive function, etc. 904
A proof of $A = B$ is obtained by transforming both sides and applying the only constructor of the type $=$, which is Refl of x * x (not Coq syntax, but you should get it). So, all proofs by tactic actually expand into programs!
* In other words, Coq tactics are just another style of programming. You can use Definition and/or Fixpoint to write proofs, or use Proof to write programs. Of course, you should not do so; but you can.
* CompCert is indeed proved against a formal specification. Which one? The official C programming language specification! Of course, you can't really prove anything against the text of the specification, so they encoded the specification in Coq using Definitions and Inductives.
In Software Foundations, there are examples of verifying a few toy interpreters and some toy programs, as well as more serious examples of verifying algorithms like red-black tree insertions and graph coloring. It does a pretty good job of explaining what and how to prove when you are writing programs in Coq. I would suggest that you start from there. 904