We study the relationship between two approaches to higher-order program verification: a semi-automated method using Dijkstra monads and a fully automated method using a higher-order fixpoint logic called HFL(Z). Although the origins of both approaches are quite different, there are some striking similarities: both convert programs to corresponding predicate transformers, and the conversion is essentially obtained by a CPS transformation. After reviewing the two approaches, we formalize an exact correspondence between the two for a restricted fragment of a functional language. We also point out that, outside the restricted fragment, there are some important differences between the two approaches, suggesting the need for cross-fertilization to obtain the best of the two approaches. As an example of the cross-fertilization, we also propose a semi-automated verification method, which requires less annotations than the Dijkstra monad approach and can scale to larger programs than the HFL(Z) approach.