Hacker News Reader

Comment by bennofs | Hacker News Reader

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.

View on HN

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.

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.

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?

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.ht...

This is used by compcert: https://compcert.org/

Yes, I know, I mentioned the extraction.

My question was whether it can help detecting translation errors from the first step.

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.

Reply on news.ycombinator.com