Leo considered several languages for implementation, including Ocaml. While I'm certain his familiarity with C++ played a big part in the final decision, he has very justified reasons for choosing it. He claims that it's extremely hard to get excellent performance without breaking the nice abstractions built by such languages (memory management, data structure layout etc.), and I have to say, Lean is blindingly fast when type-checking. A lot of things become easy when working with such a mainstream language, like writing FFI bindings and using compiler frameworks.