One of the major open questions in complexity theory is whether poly-size boolean circuits are more powerful than poly-size boolean formulas (that is, whether NC^1 is different from P). The *monotone* version of this separation was proved over 20 years ago by Karchmer and Widgerson. In this talk, we present results giving the first separation of formulas vs. circuits in the *bounded depth* setting. This separation comes via a novel lower bound for STCONN(k(n)), the problem of determining whether a graph of size n contains a path of length \leq k(n) between two distinguished vertices. We show that solving STCONN(k(n)) on unbounded fan-in boolean FORMULAS of depth \leq log(n)/polyloglog(n) requires size n^Omega(log k) for all k(n) \leq loglog(n) (in contrast, this problem has poly-size CIRCUITS of depth only O(log k)). In addition to separating the power of formulas vs. circuits up to depth logloglog(n), this implies a tight lower bound of Omega(log k) on the depth of poly-size circuits for STCONN(k(n)), improving a previous Omega(loglog k) lower bound of Beame, Impagliazzo and Pitassi [FOCS 1995].