You are praising Lean for optional verification. They want to add optional verification to OCaml. Where do you see an impedance mismatch? Just in the fact that you don't find OCaml pretty enough?