We give here a new proof of Herbrand's theorem in PAω : we use a forcing transformation to add a Cohen real to PAω. This new real allows us to avoid using the fan theorem and requiring an order on atomic formulas. We then take a look at the program extracted from this new proof using Krivine's translation of forcing into classical realizability. Because of the clever uses (i.e. only in the forcing universe) of classical logic in the proof, the extracted program does not backtrack the tree it builds, contrary to a classical proof without forcing.