6 ms·

Yes, that is a limitation. But this limitation is not too bad. In many cases, a bug in the translation simply makes the proof impossible. Somebody then investi

Yes, that is a limitation. But this limitation is not too bad. In many cases, a bug in the translation simply makes the proof impossible. Somebody then investigates why the proof does not go through and finds the bug in the translation. We only have a problem if the bug in the translation specificially cancels a bug in the original code. If there is no systematic risk, it is quite unlikely that two bugs cancel each other in this way.

user2342 2y ago
In case of coq-to-ocaml: is it feasible to do an extraction to OCaml on the translated code and compare it with the original?
- cccbbbaaa 2y ago
  You can write programs in Coq and extract them in OCaml with the `Extraction' command: https://coq.inria.fr/doc/v8.19/refman/addendum/extraction.html https://coq.inria.fr/doc/v8.19/refman/addendum/extraction.ht... This is used by compcert: https://compcert.org/ https://compcert.org/
  - user2342 2y ago
    Yes, I know, I mentioned the extraction. My question was whether it can help detecting translation errors from the first step.
    - cccbbbaaa 2y ago
      I'm not sure which first step you are talking about. Typically, one would write the program directly in Coq and use the extracted code as-is.
im3w1l 2y ago
Let's say you want to check if use after free can ever occur. Your translation is bugged and translates the whole program to a single "nop". Then the verifier happily asserts that the translated program does not cause use after free. I doubt the translation would be that bad but it could have more subtle issues of the same kind.
- bennofs 2y ago
  My argument is that you typically also check other properties, like properties describing what your program should do. These other properties likely wouldn't be satisfied by a nop program, and hopefully the same is true for many subtle issues.

6 ms·

Yes, that is a limitation. But this limitation is not too bad. In many cases, a bug in the translation simply makes the proof impossible. Somebody then investi

by bennofs 2y ago

user2342 2y ago
In case of coq-to-ocaml: is it feasible to do an extraction to OCaml on the translated code and compare it with the original?
- cccbbbaaa 2y ago
  You can write programs in Coq and extract them in OCaml with the `Extraction' command: https://coq.inria.fr/doc/v8.19/refman/addendum/extraction.html https://coq.inria.fr/doc/v8.19/refman/addendum/extraction.ht... This is used by compcert: https://compcert.org/ https://compcert.org/
  - user2342 2y ago
    Yes, I know, I mentioned the extraction. My question was whether it can help detecting translation errors from the first step.
    - cccbbbaaa 2y ago
      I'm not sure which first step you are talking about. Typically, one would write the program directly in Coq and use the extracted code as-is.
im3w1l 2y ago
Let's say you want to check if use after free can ever occur. Your translation is bugged and translates the whole program to a single "nop". Then the verifier happily asserts that the translated program does not cause use after free. I doubt the translation would be that bad but it could have more subtle issues of the same kind.
- bennofs 2y ago
  My argument is that you typically also check other properties, like properties describing what your program should do. These other properties likely wouldn't be satisfied by a nop program, and hopefully the same is true for many subtle issues.