The aim of this talk is to introduce the audience to the Halpern-Lauchli theorem, which is a Ramsey-theoretic statement about products of trees. We will discuss several applications of the theorem and outline a number of different proofs. While the original proof was combinatorial in nature, there are now a number of proofs that interact with ideas from set-theoretic forcing. One of these proofs is new, and is joint work with Chris Lambie-Hanson.