Gini index is quite often used in constructing decision trees in data mining for attribute selection and attribute split point. Is Gini coefficient just a heuristic or can we formally explain why it's defined the way it is?
I don't have a formal proof for you.
But from a quick look, the Gini is the probability of two randomly chosen items having the same type, isn't it? That sounds like a way to formally derive it from a simple, probabilistic model.
At least for the variant of Gini that I use mostly, which is this one:
where $p_i$ is the probability of class $i$ occurring. For this index, $1$ indicates a pure result, and $0$ would be maximal impurity. Some people use $1-G$ for consistency with other measures, but that obviously does not make a whole lot of a differences - it's just the opposite probability.
Gini index defined for a discrete probability distribution is a measure for inherent 'randomness' in the distribution. For a two class problem, with probabilities $p, 1-p$, it is given by $2p(1-p)$. All the outcomes belong to the same class, if $p$ equals 0 or 1 in which case the randomness in the distribution is 0. This is captured by Gini, which evaluates to zero in these cases. One can also intuitively see that for $p=1/2$ we have maximum 'randomness' and the Gini criteria rightly peaks at this point.
Interpreting it as a probability it represents the probability that two consecutively drawn labels are different. Answer by @anony-mousse explains this further in general case.