We provide a computer verified exact monadic functional implementation of the Riemann integral in constructive type theory. This may be seen as the beginning of the realization of Bishop's vision to use constructive mathematics as a high level programming language for exact analysis.