We will discuss Harrington's conceptually simple proof of the Halpern-Läuchli theorem using the machinery of forcing. Also if time permits, we will also briefly discuss its role in establishing the theorem due to Halpern and Lévy: the Boolean Prime Ideal Theorem does not imply the Axiom of Choice over ZF.