CIRCLE WITH A DOT

@MartinEscardo Re: trusting C code, I heard horror stories about compilers for aeronautics, where one of the criteria for acceptance is that the "compiler" is very transparent and that the assembly code is auditable on its own. Apparently, getting these sort of people to accept an optimising compiler, even CompCert, was a hard battle… (But it was won!)

@markusde I guess it says that :
- the definitions give you objects which once roundtripped are isomorphic to the original ones ; not the best specification, but rather solid (it rules out everything being unit or something, and is especially fine if you also translate the various operations/basic proofs which encode that they behave the way one expects)
- the lemmas you admit on the Lean side are logically equivalent (up to Lean -> Rocq translation) to ones which are proven, which to me makes them very reasonable to assume

Of course that brings the Lean -> Rocq translation to the TCB, as well as Rocq, but I still feel this is ok?

And I don't see how the liking with other Lean code changes anything, you can treat the translated code as some sort of opaque module with a bunch of definitions and proofs and use that opaquely, just as you would any other Lean module? Except in this one the proofs are not there, they're on the Rocq side

@markusde Isn't the point that having a proof on the Rocq side + a proof that the statement translated from Lean is equivalent to the Rocq one makes it reasonable to not translate the whole proof? I find it not quite fully satisfying, but the approach sounds honestly very reasonable to me.

@markusde Have you seen what can be done with this nowadays https://theoremlabs.com/blog/lf-lean/ ?