Lambda the Ultimate

Prop and Type are separated in Coq using the sorting system, while Epigram for example separate it by embedding a new, closed prop datatype into Type so all prop's begins with a particular constructor. With Coq's way it is easy to separate logical and computational terms, which forms the basis of extraction: you just need to erase things whose sort is Prop. It is also possible this way to have particular typing rules for handling props and selectively make the Prop universe impredicative for example [(∀ P : Prop, P \/ ~ P) : Prop].
The formation rules for Prop and Type are roughly the same otherwise so you can have a copy of nat, tree or whatever in one or the other. However, things in Prop intuitively obey the proof-irrelevance principle which says that in your copy of bool in Prop you will have true_prop = false_prop.

In fact, not all type systems/logical frameworks do separate them: the original version of Martin-Loef's intensional type theory did not, although many systems based on it do add the distinction, typically, as Mathieu said, to get the right notion of proof equivalence.

There's a strong technical reason to separate them in impredicative type theory, which is that several desirable type formers, most importantly impredicative Sigma quantification, cannot be added to the theory without inconsistency. This is, of course, catastrophic in Prop, but may be tolerated in Type, so such type formers can be used in Type, but forbidden in Prop, recovering consistency in the parts that matter.

I have the idea that this is in Coquand's "Metamathematical Investigations of a Calculus of Constructions", but I have lost my copy. It's discussed in Zhaohui Luo's "Computation & Reasoning".