Comment by Ohentis
13 hours ago
Most of this feels fairly orthogonal to the question asked. And the reasons lean are chosen are fairly simple: it is designed to also be used for programming and it's actually successful. Compiling to C is fairly obviously a bad choice (well I guess not obviously, people keep implementing languages this way for some reason) but arguably one of the least important factors in choosing which prover to use. The alternatives to lean would be Idris (which is both unsound and unpopular), ats (which is unpopular) or rocq (which is more reasonable but still is mostly an academic project).
Compiling to C seems obviously an excellent choice for compiling a language to. It is a good choice as a target language, and one can rely on a lot of existing tooling, a stable standard, good interoperability, and wide platform support. It is also simply enough to be modeled precisely.