3 ms·
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
by alimw 10y ago
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 :)
- tedks 10y agoI'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.
- alimw 10y agoThanks 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!