Efficient real computation in constructive type theory In 1967 Bishop proposed to use constructive analysis as a language for exact real computations. Martin-L"of proposed constructive type theory as an actual programming language. This language now forms the base of both proof assistants and programming languages. I will report on our effort to actually carry out this research program: we provide an efficient computer verified implementation of exact real numbers in the Coq proof assistant.