In context:

> Nonetheless, almost any interesting certified programming project will benefit from some activity that deserves to be called proving, and many interesting projects absolutely require semi-automated proving, to protect the sanity of the programmer. Informally, proving is unavoidable when any correctness proof for a program has a structure that does not mirror the structure of the program itself. An example is a compiler correctness proof, which probably proceeds by induction on program execution traces, which have no simple relationship with the structure of the compiler or the structure of the programs it compiles. In building such proofs, a mature system for scripted proof automation is invaluable.

What this means is that the proof of the compiler's correctness will often look different from the implementation of the compiler, and the proof language can and should have different structure and produce different output. Isomorphic doesn't mean identical.

But, this section also doesn't refer to program extraction. That's introduced later. In the program extraction world, rather than having a program, and a proof of that program, you start with the proof, encode the program behavior into the proof, and extract the program mechanically from the proof. Keep reading and you'll see how :-)

Edit: Even more context, for those unfamiliar with coq:

> In comparisons with its competitors, Coq is often derided for promoting unreadable proofs. It is very easy to write proof scripts that manipulate proof goals imperatively, with no structure to aid readers. Such developments are nightmares to maintain, and they certainly do not manage to convey "why the theorem is true" to anyone but the original author. One additional (and not insignificant) purpose of this book is to show why it is unfair and unproductive to dismiss Coq based on the existence of such developments.

Coq has a proof language that's very powerful, and very rich, but can also be very obtuse at times. Because a single proof statement might discharge a number of proof goals without really making it clear how, and because you can write your own proof "tactics" (functions/macros, essentially), you can write a proof that looks totally different from the program you could extract from it. Nevertheless, the fact that you can extract the program proves that the information required to construct the one gives you the other -- they're isomorphic. (We currently lack the tools to go from a correct program to the proof of the same, but this is a statement about ourselves, not about the correct program, modulo incompleteness.)

I skimmed the subsequent chapter to its end where program extraction comes up. It is invoked on a function called tcompile, defined on page 35. Meanwhile the theorem about the correctness of tcompile, called tcompile_correct, has only been stated on p.36 and concluded on p.37.

The program extracted from tcompile is surely independent of its proof of correctness tcompile_correct. I suppose that by the Curry-Howard isomorphism there must be some program corresponding to tcompile_correct, but it's probably not a compiler...

We may be talking at cross-purposes :)

I'm afraid I don't know enough about dependent types and PL theory to really explain this well, but bear in mind that you're on page 35. You can use program extraction on a proof itself and yield an executable program. You can use program extraction on anything in Coq, so if you use it as an implementation language you can compile it down to OCaml (or Rust now!) after proving your implementation correct.

I suppose it's possible that there are only some programs and proofs amenable to being written that way, but also suspect that's more due to the human difficulty than anything else.

Thanks but I only wanted to point out that there is a real dichotomy between an implementation and its proof of correctness, even up to isomorphism. But I maybe misunderstood what was being discussed!

Thanks, that clarifies it for me. I was making the mistake of looking at OCaml as the implementation language for the two languages, Rust and Coq, and overlooking the abstractions built on top.

Yes, isomorphic, but not identical.