Derived proofs of elementary homological algebra theorems? I know basically the definition and very general-not-so-useful properties of derived categories, and to build a deeper understanding of them, I'd like to see if it can help in re-thinking some basic results in homological algebra. 
More specifically, I'd like to know if the theory of derived categories can help in proving (perhaps some improvements of) the following : the universal coefficients formulas (homological with $\otimes$ and cohomological with $\hom$) and/or the (algebraic) Künneth formula. 
It seems reasonable enough that there should be more conceptual proofs of these (or generalizations) through derived categories, but I haven't found one (which indicates either that it doesn't exist, or is a good witness of my lack of practice).
Perhaps there would be a way to get spectral sequences from an abstract "derived" argument, to get to a more concrete thing that would be one of these theorems ? If so I'd like to see that as well, as I still haven't quite seen how to get spectral sequences from derived stuff (and it seems to be a general theme)
 A: The derived category of abelian groups is somewhat special that makes the Künneth and universal coefficient theorems take an unusually special form. 
An abstract way to state this property is
Theorem: Every element of the derived category of abelian groups is the direct sum of one-term complexes
Proof: Every chain complex is quasi-isomorphic to a complex of free abelian groups. And if $C_\bullet$ is a complex of free abelian groups, the fact every subgroup of a free abelian group is free implies you can decompose $C_n = \ker(\partial_n) \oplus \mathrm{im}(\partial_n)$, and thus you can decompose $C_n$ into a direct sum of complexes of the form $\mathrm{im(\partial_n)} \to \ker(\partial_{n-1})$, each of which is isomorphic to the one-term complex $H_{n-1}(C_\bullet)$ concentrated in degree $n-1$. $\square$
In particular, the equivalence class of every chain complex $C_\bullet$ includes the complex
$$ \ldots  \xrightarrow{0} H_1(C_\bullet) \xrightarrow{0} \underline{H_0(C_\bullet)} \xrightarrow{0} H_{-1}(C_\bullet) \xrightarrow{0} \ldots $$
which, of course, breaks apart into the direct sum of its individual terms.

From the form of tor and ext for one-term complexes, we can then write
$$ H_n (C_\bullet \otimes^\mathbb{L} D_\bullet)
\cong H_{n-i-j} \left( \bigoplus_i \bigoplus_j H_i(C_\bullet) \otimes^\mathbb{L} H_j(D_\bullet) \right) 
\\ \cong
\bigoplus_i \bigoplus_j \begin{cases}
H_i(C_\bullet) \otimes H_j(D_\bullet) & n = i+j
\\ \mathrm{tor}(H_i(C_\bullet), H_j(D_\bullet)) & n = i+j +1
\end{cases}$$
The universal coefficient theorem is the special case where $C_\bullet$ is the complex of coefficients concentrated in degree zero. Similarly,
$$ H_n (\mathbb{R}{\hom}(C_\bullet,  D_\bullet))
\cong H_{n+i-j} \left(\prod_i \bigoplus_j \mathbb{R}{\hom}(C_i, D_j) 
\right) 
\\ \cong
\prod_i \bigoplus_j \begin{cases}
\hom(H_i(C_\bullet), H_j(D_\bullet)) & n = j-i
\\ \mathrm{ext}(H_i(C_\bullet), H_j(D_\bullet)) & n = j-i-1
\end{cases}
\\\cong
\prod_i 
\hom(H_i(C_\bullet), H_{n+i}(D_\bullet)) 
\oplus
\mathrm{ext}(H_i(C_\bullet), H_{n+i+1}(D_\bullet))
$$
With $D$ concentrated in degree zero, this becomes the familiar
$$ H_{-n} (\mathbb{R}{\hom}(C_\bullet,  D))
\cong 
\hom(H_n(C_\bullet), D) 
\oplus
\mathrm{ext}(H_{n-1}(C_\bullet), D) $$
A: I have not read it too much, but in the beggining (1.3) of this the author relates derived stuff, Künneth and spectral sequences. Thus it seems that at least this short paragraph might be something that you are searching for or at least some indication of it (not sure about the rest of the document).
A: I think that "homological functors takes shorts exact sequences to long exact sequences" is a sentence that is better written un triangulated categories. In fact, the definition of a triangle is a strange mix of the notions of short/long exact sequence. In my personal opinion, the notion of triangle is precisely the "theorem" or " principle" relating them. If you want a precise theorem, take "in a triangulated category, a representable functor is homological".
A: Since you asked for spectral sequences: the universal coefficient theorem is a special case of the change-of-rings spectral sequence. 
Given a chain complex $C$ of $R$-modules of homological type, zero in negative degrees (the homological type is a convenience, but bounded below is necessary) and an $R$-algebra $S$, we have a homological first quadrant spectral sequence with $E^2$-term
$$ E^2_{pq} = \mathrm{Tor}_p^R(S, H_q(C)) \implies H_{p+q}( S \otimes C).$$
When $R$ is a PID, then $\mathrm{Tor}_q^R = 0$ for $q \geq 2$, and the resulting spectral sequence collapses at $E^2$, yielding the familiar short exact sequences. This is essentially equivalent to the calculation in Hurkyl's answer.
In derived categorical language, this spectral sequence corresponds to computing the homology of the derived tensor product $S \otimes_R^{\mathbb L} C$ in terms of the derived tensor product of the homologies. This translates into spectral sequences: we can take a resolution of $C$ by a double complex of projective objects, tensor with $S$, and take spectral sequences associated to this double complex. 
The Künneth formula over general $R$ is the same: there is a spectral sequence
$$E^2_{pq} = \bigoplus_{q_1 + q_2 = q} \mathrm{Tor}^R_p (H_{q_1}(C_1), H_{q_2}(C_2)) \implies H_{p+q}(C_1 \otimes C_2).$$
