F* is a programming language providing proof-assistant features such as dependent types, a rich logic with universes and tactics. Its primary goal is to implement security critical program e.g. cryptographic primitives (HACL*) or protocols (HTTPS in MiTLS), prove gradually their correction and extract to performant effectful low-level code. In order to achieve gradual proof of effectful code, F* relies on weakest-precondition indexed monads called Dijkstra monads. In this presentation we will explain why and how Dijkstra monads are used in F*, as well as how they are often derived from usual presentations of monads as can be found in more mainstream language such as Haskell.